simp [starUnbounded, models_iff]
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ℕ ⊧ₘ* starUnbounded c
c : ℕ
this✝⁴ : Structure Language.unit ℕ := modelStar c
this✝³ : Structure.Zero ℒₒᵣ⋆ ℕ
this✝² : Structure.One ℒₒᵣ⋆ ℕ
this✝¹ : Structure.Add ℒₒᵣ⋆ ℕ
this✝ : Structure.Eq ℒₒᵣ⋆ ℕ
this : Structure.LT ℒₒᵣ⋆ ℕ
⊢ ∀ (i : Fin c), ↑i < Semiterm.Operator.val Semiterm.Operator.Star.star ![]