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

When one of the bounds is entirely contained within the other, the union simplifies to the larger bounds. Otherwise it cannot be simplified.

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

Equationally

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

When `s₂ ⊆ s₁ ∧ t₁ ⊆ t₂`, transitivity lets us expand from the "smaller" bounds (`s₁` and `t₁`) to the "larger" bounds (`s₂` and `t₂`):

⟦s₁..t₁ ∨ s₂..t₂⟧
  = {x | (s₁ ⊆ x ∧ x ⊆ t₁) ∨ (s₂ ⊆ x ∧ x ⊆ t₂)}
  = {x | (s₂ ⊆ x ∧ x ⊆ t₂) ∨ (s₂ ⊆ x ∧ x ⊆ t₂)}
  = {x | s₂ ⊆ x ∧ x ⊆ t₂}
  = ⟦s₂..t₂⟧