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 ↔ ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y
Tactic:
unfold BoundedFormula.isNat
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.isInductive (Sum.inr (Fin.last n)))
          (BoundedFormula.mem (termSucc x) (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.all
        (BoundedFormula.imp (BoundedFormula.isInductive (Sum.inr (Fin.last n)))
          (BoundedFormula.mem (termSucc x) (Sum.inr (Fin.last n)))))
      v l ↔
    ∀ (y : V), Inductive y → interpretTerm V v l x ∈ y
Tactic:
simp
State after:
no goals