Lemma subtype_notEqual_containedIn {X:UU} (S T : hsubtype X) : S ⊆ T -> S ≢ T -> T ⊈ S. Proof. intros ci ne. apply (squash_to_hProp ne); clear ne; intros [n|n]. - apply (squash_to_hProp n); clear n; intros [x [p q]]. apply fromempty. change (neg (T x)) in q. apply q; clear q. apply (ci x). exact p. - exact n. Defined.