(G : Group) (s : A -> G) : Words -> G. Proof. intro xs. induction xs as [|x [|y xs] IHxs]. - exact mon_unit. - exact (word_rec G s x). - exact (word_rec G s x * IHxs). Defined.
Require Import Basics Types Group Subgroup