proposition: Fact ra_beta_val a n : ⟦ra_beta⟧ (a##n##vec_nil) (beta a n).
proof: Proof. exists (decomp_l a##decomp_r a##n##vec_nil); split. { apply ra_godel_beta_val. } pos split; simpl; auto; exists (a##vec_nil); split; auto; pos split; simpl; 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(recalg recomp beta ra_utils ra_recomp)