Theorem: LO.FirstOrder.Semiformula.eval_bexLE (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.LE L
inst✝¹ : LE M
inst✝ : Structure.LE L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexLE t p) ↔ ∃ x ≤ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [bexLE]
State after:
no goals