Lemma subtype_notEqual_to_negEqual {X:UU} (S T : hsubtype X) : S ≢ T -> ¬ (S ≡ T). Proof. intros n. apply (squash_to_prop n). + apply isapropneg. + intros [c|c]. * apply (squash_to_prop c). ** apply isapropneg. ** intros [x [Sx nTx]] e. use nTx; clear nTx. exact (pr1 (e x) Sx). * apply (squash_to_prop c). ** apply isapropneg. ** intros [x [Tx nSx]] e. use nSx; clear nSx. exact (pr2 (e x) Tx). Defined.