proposition: Lemma subtype_containment_isPartialOrder X : isPartialOrder (@subtype_containedIn X).
proof: Proof. use make_dirprod. - apply subtype_containment_ispreorder. - apply subtype_containment_isantisymm. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions