(x : Words) : amal_eta (word_inverse x ++ x) = mon_unit. 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 <- app_assoc. 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 <- app_assoc. refine (amal_mu_K _ _ _ _ @ _). rewrite left_inverse. rewrite amal_omega_K. apply IHxs. Defined.
Require Import Basics Types. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. Require Import WildCat.