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