Theorem: LO.FirstOrder.Semiformula.val_operator_or (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₁.or o₂).val v ↔ o₁.val v ∨ o₂.val v
Tactic:
simp [Operator.or, Operator.val]
State after:
no goals