Lemma free_gr_hrel_in_rev {X : hSet} (x : X ⨿ X) : free_gr_hrel X (coprodcomm X X x::x::[]) []. Proof. pose (H := free_gr_hrel_in (coprodcomm X X x)). rewrite coprodcomm_coprodcomm 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.