Theorem: LO.FirstOrder.Arith.Model.eval_bexLTSucc (Arithmetization/Vorspiel/Lemmata.lean)

State before:
M : Type u_1
inst✝¹⁴ : Zero M
inst✝¹³ : One M
inst✝¹² : Add M
inst✝¹¹ : Mul M
inst✝¹⁰ : LT M
inst✝⁹ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
L : Language
inst✝⁸ : L.LT
inst✝⁷ : L.Zero
inst✝⁶ : L.One
inst✝⁵ : L.Add
inst✝⁴ : Structure L M
inst✝³ : Structure.LT L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
ξ : Type u_2
n : ℕ
e : Fin n → M
ε : ξ → M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
⊢ (Semiformula.Evalm M e ε) (Semiformula.bexLTSucc t p) ↔ ∃ x ≤ valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
Tactic:
simp [Semiformula.eval_bexLTSucc, lt_succ_iff_le]
State after:
no goals