Theorem: SetTheory.interpret_succClosed (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.succClosed x) v l ↔ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
unfold BoundedFormula.succClosed
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.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.eqSucc (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)))))))
      v l ↔
    ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x

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.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.exists
            (BoundedFormula.and
              (BoundedFormula.eqSucc (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }))
              (BoundedFormula.mem (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc x)))))))
      v l ↔
    ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
simp
State after:
no goals