(x : Words) (a : A + A) (y : Words) : freegroup_eta (x ++ [a] ++ [a^] ++ y) = freegroup_eta (x ++ y). Proof. apply path_Tr, tr. exact ((cglue (x, a, y))). Defined.
Require Import Basics Types Group Subgroup