`{Funext} {σ : Signature} {A : Carriers σ} {w : SymbolType σ} : ∀ (f g : Operation A w), (∀ a : FamilyProd A (dom_symboltype w), ap_operation f a = ap_operation g a) -> f = g := match w with | [:s:] => λ (f g : A s) p, p tt | s ::: w' => λ (f g : A s → Operation A w') p, path_forall f g (λ x, (f x) (g x) (λ a, p (x,a))) end.
Require Import Import ne_list.notations.