Theorem: LO.FirstOrder.Semiformula.eval_operator₄ (Arithmetization/Vorspiel/Vorspiel.lean)

State before:
ξ : Type u_3
L : Language
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
n : ℕ
ε : ξ → M
e : Fin n → M
o : Operator L 4
t₁ t₂ t₃ t₄ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) ↔
    o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃, Semiterm.val s e ε t₄]
Tactic:
simp [eval_operator]
State after:
no goals