∀ {f : Ordinal.{u} → Ordinal.{u}},
  Order.IsNormal f →
    ∀ {a o : Ordinal.{u}},
      Order.IsSuccLimit a →
        ∀ {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}},
          a.IsFundamentalSequence o g → (f a).IsFundamentalSequence o fun b hb => f (g b hb)