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

When the "pivot" of the incomparable constraint is not comparable with either bound of the range constraint, the incomparable constraint subsumes the range constraint. Otherwise the union cannot be simplified.

(s₁..t₁) ∨ (≁ t₂) = (≁ t₂)              if s₁ ≁ t₂ ∧ t₁ ≁ t₂
                  = (s₁..t₁) ∨ (≁ t₂)   otherwise

Equationally

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

When `s₁ ≁ t₂ ∧ t₁ ≁ t₂`:

[s₁ ≁ t₂ ∧ t₁ ≁ t₂]⁰                           [s₁ ≁ t₂ ∧ t₁ ≁ t₂]⁰
───────────────────                            ───────────────────
   ⋮                    [s₁ ⊆ x ∧ x ⊆ t₁]¹                    ⋮
   ⋮                    ─────────────────                     ⋮
   ⋮     [x ⊆ t₂]³      s₁ ⊆ x     x ⊆ t₁      [t₂ ⊆ x]³      ⋮
   ⋮     ─────────────────────     ────────────────────       ⋮
s₁ ⊈ t₂        s₁ ⊆ t₂                   t₂ ⊆ t₁           t₂ ⊈ t₁
──────────────────────                   ─────────────────────────
        false              [x ~ t₂]²               false
          ⋮            ───────────────               ⋮
          ⋮            x ⊆ t₂ ∨ t₂ ⊆ x               ⋮
        ────────────────────────────────────────────────³
                            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₂ ∧ t₁ ≁ t₂) → ⟦s1..t₁⟧ ∪ ⟦≁ t₂⟧ = ⟦≁ t₂⟧