proposition: Lemma word_concat_wV x : freegroup_eta (x @ word_change_sign x) = mon_unit.
proof: Proof. set (x' := word_change_sign x). rewrite <- (word_change_sign_inv x). change (freegroup_eta (word_change_sign x' @ x') = mon_unit). apply word_concat_Vw. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list