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