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