fact: Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C := fix go l1 l2 := match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)