x : freegroup_eta (word_change_sign x ++ x) = mon_unit. Proof. induction x. 1: reflexivity. lhs nrapply (ap (fun x => freegroup_eta (x ++ _))). 1: nrapply reverse_cons. change (freegroup_eta ((word_change_sign x ++ [a^]) ++ [a] ++ x) = mon_unit). lhs_V nrapply ap. 1: nrapply app_assoc. set (a' := a^). rewrite <- (change_sign_inv a). lhs nrapply freegroup_tau. apply IHx. Defined.
Require Import Basics Types Group Subgroup