proposition: Fact fun2vec_vec2fun n v x : fun2vec 0 n (@vec2fun n v x) = v.
proof: Proof. apply vec_pos_ext. intros p; rewrite vec_pos_fun2vec; simpl. unfold vec2fun. generalize (pos2nat_prop p). destruct (le_lt_dec n (pos2nat p)); try lia. rewrite nat2pos_pos2nat; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)