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

State before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
o₁ o₂ : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (o₁.or o₂).operator v = o₁.operator v ⋎ o₂.operator v
Tactic:
simp [operator, or]
State after:
no goals