proposition: Lemma subtype_containment_ispreorder X : ispreorder (@subtype_containedIn X).
proof: Proof. use make_dirprod. - apply subtype_containment_istrans. - apply subtype_containment_isrefl. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions