Union of `s₁..t₁` or `≠ t₂`

When the range constraint contains the "hole" from the non-equivalent constraint, then the result is always satisfiable. Otherwise the range constrant is subsumed by the non-equivalent constraint.

(s₁..t₁) ∨ (≠ t₂) = 𝟙       is s₁ ⊆ t₂ ∧ t₂ ⊆ t₁
                  = (≠ t₂)  otherwise

Equationally

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

When `s₁ ⊆ t₂ ∧ t₂ ⊆ t₁`, transitivity lets us show that `t₂ ⊆ x` and `x ⊆ t₂`, which shows that `t₂` is in the result. The `≠ t₂` constraint adds every other type to the result as well.

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

When `t₂ ⊂ s₁`:

  [s₁ ⊆ x ∧ x ⊆ t₁]¹
  ─────────────────
       s₁ ⊆ x         [t₂ ⊂ s₁]⁰
       ────────────────────────
               t₂ ⊂ x
               ──────
               x ≠ t₂
     ──────────────────────────¹
     (s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
          ─────────────────
          ⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
     ──────────────────────────
     ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
────────────────────────────────────⁰
t₂ ⊂ s₁ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧

When `s₁ ≁ t₂`:

[s₁ ⊆ x ∧ x ⊆ t₁]¹  [x = t₂]²
─────────────────   ────────
     s₁ ⊆ x          x ⊆ t₂     [s₁ ≁ t₂]⁰
     ──────────────────────     ─────────
            s₁ ⊆ t₂              s₁ ⊈ t₂
            ────────────────────────────
                       false
                       ──────²
                       x ≠ t₂
            ──────────────────────────¹
            (s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
       ────────────────────────────────────
       {x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
                 ─────────────────
                 ⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
            ──────────────────────────
            ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
       ────────────────────────────────────⁰
       s₁ ≁ t₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧

When `t₁ ⊂ t₂`:

  [s₁ ⊆ x ∧ x ⊆ t₁]¹
  ─────────────────
       x ⊆ t₁         [t₁ ⊂ t₂]⁰
       ────────────────────────
               x ⊂ t₂
               ──────
               x ≠ t₂
     ──────────────────────────¹
     (s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
────────────────────────────────────
{x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
          ─────────────────
          ⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
     ──────────────────────────
     ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
────────────────────────────────────⁰
t₁ ⊂ t₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧

When `t₁ ≁ t₂`:

[s₁ ⊆ x ∧ x ⊆ t₁]¹  [x = t₂]²
─────────────────   ────────
     x ⊆ t₁          t₂ ⊆ x     [t₁ ≁ t₂]⁰
     ──────────────────────     ─────────
            t₂ ⊆ t₁              t₂ ⊈ t₁
            ────────────────────────────
                       false
                       ──────²
                       x ≠ t₂
            ──────────────────────────¹
            (s₁ ⊆ x ∧ x ⊆ t₁) → x ≠ t₂
       ────────────────────────────────────
       {x | s₁ ⊆ x ∧ x ⊆ t₁} ⊆ {x | x ≠ t₂}
                 ─────────────────
                 ⟦s1..t₁⟧ ⊆ ⟦≠ t₂⟧
            ──────────────────────────
            ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧
       ────────────────────────────────────⁰
       t₁ ≁ t₂ → ⟦s1..t₁⟧ ∪ ⟦≠ t₂⟧ = ⟦≠ t₂⟧