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

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqSucc x y) v l ↔ interpretTerm V v l x = succ (interpretTerm V v l y)
Tactic:
unfold BoundedFormula.eqSucc succ
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqSingleton (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqUnion (termSucc x) (termSucc y) (Sum.inr (Fin.last n)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ {interpretTerm V v l y}

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.eqSingleton (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqUnion (termSucc x) (termSucc y) (Sum.inr (Fin.last n)))))
      v l ↔
    interpretTerm V v l x = interpretTerm V v l y ∪ {interpretTerm V v l y}
Tactic:
simp
State after:
no goals