Theorem: LO.FirstOrder.Semiformula.eval_bexLTSucc (Logic/FirstOrder/Arith/Basic.lean)

State before:
n : ℕ
L : Language
inst✝⁹ : L.LT
inst✝⁸ : L.Zero
inst✝⁷ : L.One
inst✝⁶ : L.Add
ξ : Type u_1
M : Type u_2
s : Structure L M
inst✝⁵ : LT M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Structure.LT L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexLTSucc t p) ↔ ∃ x < val s e ε t + 1, (Eval s (x :> e) ε) p
Tactic:
simp [bexLTSucc, Operator.numeral]
State after:
no goals