¶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.