have : ℕ⋆ ⊧ₘ (“!!(Semiterm.Operator.numeral ℒₒᵣ⋆ n) < ⋆” : Sentence ℒₒᵣ⋆) :=
  models_union_trueArithWithStarUnbounded.realize
    (Set.mem_iUnion_of_mem (n + 1) (Set.mem_union_right _ $ Set.mem_range_self $ Fin.last n))
n : ℕ
⊢ ↑n < ⋆
n : ℕ
this :
  ℕ⋆ ⊧ₘ
    (“!!(Semiterm.Operator.const (Semiterm.Operator.numeral ℒₒᵣ⋆ n)) <
        !!(Semiterm.Operator.const Semiterm.Operator.Star.star)”)
⊢ ↑n < ⋆