proposition: Lemma generated_free_gr_hrel_in {X : hSet} (l : free_monoid (setcoprod X X)) : generated_binopeqrel (free_gr_hrel X) (l * fginv l) [].
proof: 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.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists