(f : ∀ s, A s → B s) {w : SymbolType σ} (a : FamilyProd A (dom_symboltype w)) (α : Operation A w) (β : Operation B w) (P : OpPreserving f α β) : f (cod_symboltype w) (ap_operation α a) = ap_operation β (map_family_prod f a). Proof. induction w. - assumption. - destruct a as [x a]. apply IHw. apply P. Defined.
Require Import Import algebra_notations ne_list.notations.