proposition: Lemma amal_eta_word_concat_Vw (x : Words) : amal_eta (word_inverse x ++ x) = mon_unit.
proof: Proof. induction x as [|x xs]. 1: reflexivity. destruct x as [h|k]. + change (amal_eta (word_inverse ([inl h] ++ xs) ++ [inl h] ++ xs) = mon_unit). rewrite word_inverse_ww. rewrite <- word_concat_w_ww. refine (amal_mu_H _ _ _ _ @ _). rewrite left_inverse. rewrite amal_omega_H. apply IHxs. + change (amal_eta (word_inverse ([inr k] ++ xs) ++ [inr k] ++ xs) = mon_unit). rewrite word_inverse_ww. rewrite <- word_concat_w_ww. refine (amal_mu_K _ _ _ _ @ _). rewrite left_inverse. rewrite amal_omega_K. apply IHxs. Defined.
imports: Basics Types Cubical Spaces.List Colimits.Pushout Truncations.Core Truncations.SeparatedTrunc Algebra.Groups.Group WildCat