Intersection of `≤ t₁` and `≁ t₂`

The intersection of an upper bound and an incomparible depends on how the two types are related.

(≤ t₁) ∧ (≁ t₂) = ∅                if t₁ ⊆ t₂
                = (≤ t₁) ∧ (≁ t₂)  otherwise

Equationally

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

If `t₁ ⊆ t₂`, the key step is that `x ⊆ t₁` implies `x ⊆ t₂` by transitivity, which contradicts the incomparible constraint on `t₂`.

⟦(≤ t₁) ∧ (≁ t₂)⟧
  = {x | x ⊆ t₁} ∩ {x | x ⊈ t₂ ∧ t₂ ⊈ x}
  = {x | x ⊆ t₁ ∧ x ⊈ t₂ ∧ t₂ ⊈ x}
  = {x | x ⊆ t₁ ∧ x ⊆ t₂ ∧ x ⊈ t₂ ∧ t₂ ⊈ x}
  = {x | x ⊆ t₁ ∧ false ∧ t₂ ⊈ x}
  = {x | false}
  = ∅

Otherwise, the two constraints cannot be simplified.