Theorem: LO.FirstOrder.Semiformula.eval_operator₁ (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 1
t : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t]) ↔ o.val ![Semiterm.val s e ε t]
Tactic:
simp [eval_operator, Matrix.constant_eq_singleton]
State after:
no goals