{w : SymbolType σ} (f : ∀ (i:I) s, C s → A i s) (α : ∀ (i:I), Operation (A i) w) (β : Operation C w) (P : ∀ (i:I), OpPreserving (f i) β (α i)) : OpPreserving (def_prod_algebra_mapin f) β (op_prod_algebra I A w (λ i, α i)). Proof. induction w. - funext i. apply P. - intro x. apply IHw. intro i. apply P. Defined.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.