(G : Group) (s : A -> G) (x y : Words) : words_rec G s (x ++ y) = words_rec G s x * words_rec G s y. Proof. induction x as [|x xs IHxs] in y |- *. - symmetry; nrapply grp_unit_l. - change ((?x :: ?xs) ++ y) with (x :: xs ++ y). lhs nrapply words_rec_cons. lhs nrapply ap. 1: nrapply IHxs. lhs nrapply grp_assoc. nrapply (ap (.* _)). symmetry. apply words_rec_cons. Defined.
Require Import Basics Types Group Subgroup