proposition: Lemma minimal_eqrel_from_hrel (R : eqrel A) (H : ∏ a b, R0 a b -> R a b) : ∏ a b, eqrel_from_hrel a b -> R a b.
proof: Proof. now intros a b H'; apply (H' _ H). Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets