proposition: Lemma free_abmonoid_hrel_univ {X : hSet} (P : free_monoid X → free_monoid X → UU) (HP : ∏ (x y : free_monoid X), isaprop (P x y)) (Hind : ∏ x y, P (x * y) (y * x)) (x y : free_monoid X) : free_abmonoid_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). induction v as (y',v). induction v as (p1,p2). induction p1. induction p2. apply Hind. Defined.
imports: UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.IteratedBinaryOperations UniMath.Combinatorics.Lists