proposition: Lemma sumofmaps_free_gr_unit {X : hSet} : sumofmaps free_gr_unit (grinv (free_gr X) ∘ free_gr_unit) ~ @presented_monoid_intro (setcoprod X X) (free_gr_hrel X).
proof: Proof. intro x. induction x as [x|x]; reflexivity. Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists