∀ {o : ONote} {x : Option ONote ⊕ (ℕ → ONote)} (e : o.fundamentalSequence = x),
  o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
    | Sum.inr f, x => fun i => (f i).fastGrowing i