proposition: Lemma isdecincltoisincl {X Y : UU} (f : X -> Y) : isdecincl f -> isincl f.
proof: Proof. intros is y. apply (isdecproptoisaprop _ (is y)). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom