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

The intersection of a range and a non-equivalent depends on how the two types are related.

(s₁..t₁) ∧ (≠ t₂) = ∅                  if s₁ = t₁ = t₂
                  = (s₁..t₁)           if s₁ ⊈ t₂ ∨ t₂ ⊈ t₁
                  = (s₁..t₁) ∧ (≠ t₂)  otherwise

Equationally

⟦s₁..t₁⟧ = {x | s₁ ⊆ x ∧ x ⊆ t₁}
⟦≠ t₂⟧   = {x | x ⊈ t₂ ∨ t₂ ⊈ x}

Case 1

If `s₁ = t₁`, then the range constraint `s₁..t₁` is actually an equivalence constraint `= s₁`; if also `s₁ = t₂`, then it's intuitive that the constraints should conflict with each other.

⟦(s..s) ∧ (≠ s)⟧
  = {x | s ⊆ x ∧ x ⊆ s} ∩ {x | x ⊈ s ∨ s ⊈ x}
  = {x | (s ⊆ x ∧ x ⊆ s) ∧ (x ⊈ s ∨ s ⊈ x)}
  = {x | (s ⊆ x ∧ x ⊆ s ∧ x ⊈ s) ∨ (s ⊆ x ∧ x ⊆ s ∧ s ⊈ x)}
  = {x | (s ⊆ x ∧ false) ∨ (false ∧ x ⊆ s)}
  = {x | false ∨ false}
  = {x | false}
  = ∅

Case 2

If `s₁ ⊈ t₂ ∨ t₂ ⊈ t₁`:

                     [s₁ ⊆ x ∧ x ⊆ t₁]¹
                     ─────────────────
           [x = t₂]²  s₁ ⊆ x   x ⊆ t₁   [x = t₂]²
           ─────────────────   ─────────────────
[s₁ ⊈ t₂]³      s₁ ⊆ t₂             t₂ ⊆ t₁        [t₂ ⊈ t₁]³
───────────────────────             ────────────────────────
         false                               false
           ⋮                                   ⋮
           ⋮       [s₁ ⊈ t₂ ∨ t₂ ⊈ t₁]⁰        ⋮
        ───────────────────────────────────────────³
                          false
                         ───────²
                          x ≠ t₂
                ──────────────────────────¹
                (s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
            ────────────────────────────────────
            {x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
                    ─────────────────
                    ⟦s₁..t₁⟧ ⊆ ⟦≠ t₂⟧
                ────────────────────────────
                ⟦s₁..t₁⟧ ∩ ⟦≠ t₂⟧ = ⟦s₁..t₁⟧
      ──────────────────────────────────────────────────⁰
      (s₁ ⊈ t₂ ∨ t₂ ⊈ t₁) → ⟦s₁..t₁⟧ ∩ ⟦≠ t₂⟧ = ⟦s₁..t₁⟧

Otherwise

Otherwise, the two constraints cannot be simplified.