proposition: Lemma path_ap_operation_ker_related {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: Proof. induction w. - reflexivity. - destruct a as [x a], b as [y b], R as [r R]. cbn. destruct r. by apply IHw. Qed.
imports: HSet Colimits.Quotient Modalities.ReflectiveSubuniverse Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra