{σ} {A : Carriers σ} {w : SymbolType σ} : Operation A w → FamilyProd A (dom_symboltype w) → A (cod_symboltype w) := match w with | [:s:] => λ f _, f | s ::: w' => λ f '(x, l), (f x) l end.
Require Import Import ne_list.notations.