proposition: Fact ra_beta_rel v e : ⟦ra_beta⟧ v e <-> e = beta (vec_pos v pos0) (vec_pos v pos1).
proof: Proof. vec split v with a; vec split v with n; vec nil v. split. + intros H; apply ra_rel_fun with (1 := H), ra_beta_val; auto. + intros; subst; apply ra_beta_val; 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)