exact hzero
case zero
n : ℕ
μ : Type v
e✝ : Fin n → ℕ
ε : μ → ℕ
p : Semiformula ℒₒᵣ ℕ 1
e : ℕ → ℕ
hzero : (Semiformula.Eval (standardModel ℕ) ![0] e) p
hsucc : ∀ (x : ℕ), (Semiformula.Eval (standardModel ℕ) ![x] e) p → (Semiformula.Eval (standardModel ℕ) ![x + 1] e) p
⊢ (Semiformula.Eval (standardModel ℕ) ![0] e) p
no goals