fact: Definition freegroup_tau (x : Words) (a : A + A) (y : Words) : freegroup_eta (x @ [a] @ [a^] @ y) = freegroup_eta (x @ y).
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list