proposition: Fact fun2vec_id i n f : fun2vec i n f = vec_set_pos (fun p => f (i+pos2nat p)).
proof: Proof. revert i; induction n as [ | n IHn ]; intros i; simpl; f_equal; auto. rewrite IHn. apply vec_pos_ext; intros; do 2 rewrite vec_pos_set; f_equal. rewrite pos2nat_nxt; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)