proposition: Lemma oppreserving_proj_prod_algebra {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: Proof. induction w. - exact P. - intro p. apply (IHw (λ i, v i (p i)) (α (p i))). f_ap. Defined.
imports: HoTT.Types.Bool HoTT.Types.Forall HoTT.Classes.theory.ua_homomorphism