simpa [←hp] using induction_eval (M := M) Cp e
case intro.intro.intro
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 : M → Prop
e : ℕ → M
p : Semiformula L ℕ 1
Cp : C p
hp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] e) p
⊢ P 0 → (∀ (x : M), P x → P (x + 1)) → ∀ (x : M), P x
no goals