Theorem: LO.FirstOrder.Semiterm.Operator.val_comp (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type w
s : Structure L M
k m : ℕ
o₁ : Operator L k
o₂ : Fin k → Operator L m
v : Fin m → M
⊢ (o₁.comp o₂).val v = o₁.val fun i => (o₂ i).val v
Tactic:
simp [comp, val, val_operator]
State after:
no goals