(x y : Words) : amal_eta (x ++ [inl mon_unit] ++ y) = amal_eta (x ++ y). Proof. unfold amal_eta. apply path_Tr, tr. exact (cglue (inl (inr (x,y)))). 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.