Theorem: LO.FirstOrder.Arith.val_lMap_oringEmb (Logic/FirstOrder/Arith/Model.lean)

State before:
n : ℕ
ξ : Type u_2
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
e : Fin n → M
ε : ξ → M
t : Semiterm ℒₒᵣ ξ n
⊢ Semiterm.valm M e ε (Semiterm.lMap oringEmb t) = Semiterm.valm M e ε t
Tactic:
simp [Semiterm.val_lMap, standardModel_lMap_oringEmb_eq_standardModel]
State after:
no goals