Theorem: SetTheory.interpret_isNat (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isNat x) v l ↔ interpretTerm V v l x ∈ ω
Tactic:
rw [mem_ω_iff, interpret_isNat']
State after:
no goals