have : M ⊧ₘ (∀ᶠ* succInd p) :=
  ModelsTheory.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
⊢ (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
C : Semiformula L ℕ 1 → Prop
inst✝ : M ⊧ₘ* Theory.indScheme L C
p : Semiformula L ℕ 1
hp : C p
v : ℕ → M
this : M ⊧ₘ ∀ᶠ* succInd p
⊢ (Semiformula.Evalm M ![0] v) p →
    (∀ (x : M), (Semiformula.Evalm M ![x] v) p → (Semiformula.Evalm M ![x + 1] v) p) →
      ∀ (x : M), (Semiformula.Evalm M ![x] v) p