proposition: Lemma generated_free_gr_hrel_in_rev {X : hSet} (l : free_monoid (setcoprod X X)) : generated_binopeqrel (free_gr_hrel X) (fginv l * l) [].
proof: Proof. pose (H := generated_free_gr_hrel_in (fginv l)). rewrite fginv_fginv in H. exact H. Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists