proposition: Lemma isaprop_hsubtype_preserving {X Y : UU} (U : hsubtype X) (V : hsubtype Y) (f : X → Y) : isaprop (hsubtype_preserving U V f).
proof: Proof. apply impred_isaprop ; intro. apply isapropimpl. apply V. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions