proposition: Lemma beta_fun_inv n f : { a | forall p, p < n -> f p = beta a p }.
proof: Proof. destruct beta_inv with (v := vec_set_pos (fun p : pos n => f (pos2nat p))) as (a & Ha). exists a; intros p Hp. specialize (Ha (nat2pos Hp)). rewrite vec_pos_set, pos2nat_nat2pos in Ha. auto. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat gcd crt sums) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recomp)