(G : Group) (s : A -> G) (a : A + A) (b c : Words) : words_rec G s (map1 (b, a, c)) = words_rec G s (map2 (b, a, c)). Proof. unfold map1, map2. rhs nrapply (words_rec_pp G s). lhs nrapply words_rec_pp. nrapply (ap (_ *.)). lhs nrapply words_rec_pp. lhs nrapply ap. 1: nrapply words_rec_pp. lhs nrapply grp_assoc. rhs_V nrapply grp_unit_l. nrapply (ap (.* _)). destruct a; simpl. - nrapply grp_inv_r. - nrapply grp_inv_l. Defined.
Require Import Basics Types Group Subgroup