(G : Group) (s : A -> G) (x : A + A) (xs : Words) : words_rec G s (x :: xs)%list = word_rec G s x * words_rec G s xs. Proof. induction xs in x |- *. - symmetry; nrapply grp_unit_r. - reflexivity. Defined.
Require Import Basics Types Group Subgroup