(g : ∀ s, B s → C s) `{!IsHomomorphism g} (f : ∀ s, A s → B s) `{!IsHomomorphism f} {w : SymbolType σ} (α : Operation A w) (β : Operation B w) (γ : Operation C w) (G : OpPreserving g β γ) (F : OpPreserving f α β) : OpPreserving (λ s, g s o f s) α γ. Proof. induction w; simpl in *. - by path_induction. - intro x. by apply (IHw _ (β (f _ x))). Defined.
Require Import Import algebra_notations ne_list.notations.