simp[Function.comp]
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
no goals