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

The intersection of an upper bound and a non-equivalence cannot be simplified.

(≤ t₁) ∧ (≠ t₂) = (≤ t₁) ∧ (≁ t₂)

(If there is also a lower bound, then the _range_ might be simplifiable!)