simp[Empty.eq_elim, succInd, models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons',
  Semiformula.eval_substs, Semiformula.eval_rew_q Rew.toS, Function.comp]
n : ℕ
μ : Type v
e : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
⊢ ℕ ⊧ₘ ∀ᶠ* succInd p
n : ℕ
μ : Type v
e : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
⊢ ∀ (ε : ℕ → ℕ),
    (Semiformula.Eval (standardModel ℕ) ![0] ε) p →
      (∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] ε) p) →
        ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] ε) p