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. pose (H := generated_free_gr_hrel_in (fginv l)). rewrite fginv_fginv in H. exact H. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Combinatorics.Lists.