Theorem: LO.FirstOrder.Semiformula.eval_ballMem (Logic/FirstOrder/Basic/Operator.lean)

State before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.Mem L
inst✝¹ : Membership M M
inst✝ : Structure.Mem L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (ballMem t p) ↔ ∀ x ∈ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [ballMem]
State after:
no goals