proposition: 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: 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.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists