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 3
t₁ t₂ t₃ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂, t₃]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃]
Tactic:
simp [eval_operator]
State after:
no goals