proposition: Lemma subtype_containment_isantisymm X : isantisymm (@subtype_containedIn X).
proof: Proof. intros S T i j. apply (invmap (hsubtype_univalence S T)). apply subtype_equal_cond. split; assumption. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions