proposition: Lemma isaprop_subtype_containedIn {X : UU} (U V : hsubtype X) : isaprop (subtype_containedIn U V).
proof: Proof. apply impred_isaprop ; intro. apply isapropimpl. apply V. Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions