proposition: Lemma empty_hsubtype_preserving {X Y : UU} (f : X → Y) : hsubtype_preserving (emptysubtype X) (emptysubtype Y) f.
proof: Proof. unfold hsubtype_preserving. rewrite image_hsubtype_emptyhsubtype. apply subtype_containment_isrefl. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions