fact: Definition vec_map2 {A B C} (g:A -> B -> C) : forall (n : nat), vec A n -> vec B n -> vec C n := @rect2 _ _ (fun n _ _ => vec C n) vec_nil (fun _ _ _ H a b => (g a b) ## H).
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)