∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}},
  Order.IsNormal f →
    (Ordinal.veblenWith f o₁ a < Ordinal.veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < Ordinal.veblenWith f o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblenWith f o₁ a < b)