Intersection of `s₁..t₁` and `~ t₂`

(≠ t₁) ∧ (~ t₂) = (≠ t₁) ∧ (~ t₂)

Cannot be simplified, even when `t₁ = t₂`. (`t ⊆ ⟦~ t⟧ ∧ t ⊈ ⟦≠ t⟧`; for any `x ≁ t`, `x ⊈ ⟦~ t⟧ ∧ x ⊆ ⟦≠ t⟧`)