x : freegroup_eta (x ++ word_change_sign x) = mon_unit. 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.
Require Import Basics Types Group Subgroup