Lemma free_gr_hrel_univ {X : hSet} (P : free_monoid (setcoprod X X) → free_monoid (setcoprod X X) → UU) (HP : ∏ x y, isaprop (P x y)) (Hind : ∏ x, P (x::coprodcomm X X x::[]) []) (x y : free_monoid (setcoprod X X)) : free_gr_hrel X x y → P x y. Proof. apply (@hinhuniv _ (make_hProp (P x y) (HP x y))). intro v. induction v as (x',v), v as (p1,p2), p1, p2. apply Hind. 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.