proposition: Lemma words_rec_coh (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: Proof. unfold map1, map2. refine (concat _ (words_rec_pp G s _ _)^). refine (concat (words_rec_pp G s _ _) _); f_ap. refine (concat _ (right_identity _)). refine (concat (ap _ (word_concat_w_ww _ _ _)^) _). refine (concat (words_rec_pp G s _ _) _); f_ap. refine (concat (concat (simple_associativity _ _ _) _) (left_identity mon_unit)). destruct a; simpl; f_ap. + apply right_inverse. + apply left_inverse. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list