∀ {e a : ONote} [Ne : e.NF] [Na : a.NF] {a' : Ordinal.{0}},
  e.repr ≠ 0 →
    a' < Ordinal.omega0 ^ e.repr →
      a.repr = a' →
        ∀ (n : ℕ+), (Ordinal.omega0 ^ e.repr * ↑↑n + a') ^ Ordinal.omega0 = (Ordinal.omega0 ^ e.repr) ^ Ordinal.omega0