simpa [models_iff, Model.numeral_eq_natCast] using this
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆
no goals