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

State before:
L : Language
M : Type w
s : Structure L M
k : ℕ
o₁ o₂ : Operator L k
v : Fin k → M
⊢ (o₁.and o₂).val v ↔ o₁.val v ∧ o₂.val v
Tactic:
simp [Operator.and, Operator.val]
State after:
no goals