Theorem: LO.FirstOrder.Arith.trueArithWithStarUnbounded.cumulative (Logic/FirstOrder/Arith/Nonstandard.lean)

State before:
c : ℕ
⊢ (fun n =>
      “!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ ↑n)) <
          !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”) =
    (fun n =>
        “!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ ↑n)) <
            !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”) ∘
      Fin.castSucc
Tactic:
simp[Function.comp]
State after:
no goals