proposition: Corollary godel_beta_fun_inv n f : { a : _ & { b | forall p, p < n -> f p = godel_beta a b p } }.
proof: Proof. destruct godel_beta_inv with (v := vec_set_pos (fun p : pos n => f (pos2nat p))) as (a & b & H). exists a, b; intros p Hp. specialize (H (nat2pos Hp)). rewrite vec_pos_set, pos2nat_nat2pos in H. auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd prime binomial) Undecidability.Shared.Libs.DLW.Vec(pos vec)