Lemma free_abgr_hrel_univ {X : hSet} (P : free_gr X → free_gr X → UU) (HP : ∏ (x y : free_gr X), isaprop (P x y)) (Hind : ∏ x y, P (x * y) (y * x)) (x y : free_gr X) : free_abgr_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). induction v as (y',v). induction v as (p1,p2). induction p1. induction 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.