proposition: Lemma iseqrelquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : iseqrel L) : iseqrel (quotrel is).
proof: Proof. intros. split with (ispoquotrel is (pr1 isl)). apply (issymmquotrel is (pr2 isl)). Defined.
imports: UniMath.Foundations.Propositions