Lemma subtype_notEqual_from_negEqual {X:UU} (S T : hsubtype X) : LEM -> (S ≢ T <- ¬ (S ≡ T)). Proof. intros lem ne. unfold subtype_equal in ne. assert (q := negforall_to_existsneg _ lem ne); clear ne. apply (squash_to_hProp q); clear q; intros [x n]. unfold subtype_notEqual. assert (r := weak_fromnegdirprod _ _ n); clear n. unfold dneg in r. assert (s := proof_by_contradiction lem r); clear r. apply (squash_to_hProp s); clear s. intros s. apply hinhpr. induction s as [s|s]. + apply ii1, hinhpr. exists x. now apply negimpl_to_conj. + apply ii2, hinhpr. exists x. now apply negimpl_to_conj. Defined.