{A B C} (f : A -> B -> C) (y : B) l {defl defr} : list_map2 f defl defr l (repeat y (length l)) = list_map (fun x => f x y) l. Proof. induction l as [|x l IHl]. - reflexivity. - cbn; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum