proposition: Lemma word_concat_Vw x : freegroup_eta (word_change_sign x @ x) = mon_unit.
proof: Proof. induction x. 1: reflexivity. simpl. set (a' := a^). rewrite <- (change_sign_inv a). change (freegroup_eta ((word_change_sign x @ [a']) @ ([a'^] @ x)) = mon_unit). rewrite word_concat_w_ww. rewrite freegroup_tau. apply IHx. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list