∀ (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}),
  Ordinal.veblenWith f o =
    if o = 0 then f
    else
      Ordinal.derivFamily fun x =>
        match (motive := { x // x ∈ Set.Iio o } → Ordinal.{u} → Ordinal.{u}) x with
        | ⟨x, property⟩ => Ordinal.veblenWith f x