proposition: Fact vec2fun_fun2vec n f x i : i < n -> @vec2fun n (fun2vec 0 n f) x i = f i.
proof: Proof. intros H. unfold vec2fun. destruct (le_lt_dec n i); try lia. rewrite vec_pos_fun2vec, pos2nat_nat2pos; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)