proposition: Lemma iscomprelrellogeqf1 {X : UU} {R R' : hrel X} (L : hrel X) (lg : hrellogeq R R') (is : iscomprelrel R L) : iscomprelrel R' L.
proof: Proof. intros. apply (iscomprelfun2logeqf lg L is). Defined.
imports: UniMath.Foundations.Propositions