proposition: Lemma iscomprelfunlogeqf {X Y : UU} {R L : hrel X} (lg : hrellogeq L R) (f : X -> Y) (is : iscomprelfun L f) : iscomprelfun R f.
proof: Proof. intros. intros x x' r. apply (is _ _ (pr2 (lg _ _) r)). Defined.
imports: UniMath.Foundations.Propositions