simp
V : Type u_1
inst✝ : Zermelo V
r x✝ y✝ z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.and (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc y))
          (BoundedFormula.eqOPair (termSucc x) (Sum.inr (Fin.last n)) (Sum.inr (Fin.last n)))))
      v l ↔
    ∃ z, z ∈ interpretTerm V v l y ∧ interpretTerm V v l x = opair z z
no goals