proposition: Lemma beta_inv n (v : vec _ n) : { a | forall p, beta a (pos2nat p) = vec_pos v p }.
proof: Proof. destruct (godel_beta_inv v) as (a & b & H). exists (recomp a b); intro p; unfold beta. rewrite decomp_l_recomp, decomp_r_recomp; 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)