{A B C : Type} {n} (f : A -> B -> C) : Vector A n -> Vector B n -> Vector C n := fun v1 v2 => Build_Vector C n (fun i _ => f (entry v1 i) (entry v2 i)).
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids. Require Import Types.Sigma. Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module. Require Import Spaces.Nat.Core. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import abstract_algebra.