{w : SymbolType σ} (β : Operation B w) (a b : FamilyProd A (dom_symboltype w)) (R : for_all_2_family_prod A A cong_ker a b) : ap_operation β (map_family_prod f a) = ap_operation β (map_family_prod f b). Proof. induction w. - reflexivity. - destruct a as [x a], b as [y b], R as [r R]. cbn. destruct r. by apply IHw. Qed.
Require Import Import