proposition: Lemma words_rec_pp (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: Proof. induction x. 1: symmetry; apply left_identity. cbn; rewrite <- simple_associativity. f_ap. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list