proposition: Lemma isaprop_eqrel_from_hrel a b : isaprop (∏ R : eqrel A, (∏ x y, R0 x y -> R x y) -> R a b).
proof: Proof. apply impred; intro R; apply impred_prop. Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets