{w : SymbolType σ} (i : I) (v : ∀ i : I, Operation (A i) w) (α : Operation (A i) w) (P : v i = α) : OpPreserving (def_proj_prod_algebra i) (op_prod_algebra I A w v) α. Proof. induction w. - exact P. - intro p. apply (IHw (λ i, v i (p i)) (α (p i))). f_ap. Defined.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.