have : ℕ ⊧ₘ* starUnbounded c := by
  simp [starUnbounded, models_iff]; exact Fin.prop
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ Satisfiable (trueArithWithStarUnbounded c)
c : ℕ
this✝⁵ : Structure Language.unit ℕ := modelStar c
this✝⁴ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝³ : Structure.One ℒₒᵣ⋆ ℕ
this✝² : Structure.Add ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Eq ℒₒᵣ⋆ ℕ
this✝ : Structure.LT ℒₒᵣ⋆ ℕ
this : ℕ ⊧ₘ* starUnbounded c
⊢ Satisfiable (trueArithWithStarUnbounded c)