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

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

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

Equationally

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

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

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

Otherwise, the two constraints cannot be simplified.