Lemma generated_free_gr_hrel_in {X : hSet} (l : free_monoid (setcoprod X X)) : generated_binopeqrel (free_gr_hrel X) (l * fginv l) []. Proof. intros R H. revert l. apply list_ind. - apply eqrelrefl. - intros x xs IH. change (R ((free_monoid_unit x * xs) * (fginv xs * @free_monoid_unit (setcoprod X X) (coprodcomm X X x))) []). rewrite assocax, <- (assocax _ _ _ (free_monoid_unit _)). refine (eqreltrans (pr1 R) _ _ _ (binopeqrel_resp_left R _ (binopeqrel_resp_right R _ IH)) _). apply H, free_gr_hrel_in. 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.