fact: Definition vec2fun n (v : vec X n) x i := match le_lt_dec n i with | left _ => x | right H => vec_pos v (nat2pos H) end.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)