proposition: Fact ra_project_rel n p v x : ⟦@ra_project n p⟧ v x <-> x = vec_pos (@project n (vec_head v)) p.
proof: Proof. vec split v with a; vec nil v. split. + intros H; apply ra_rel_fun with (1 := H), ra_project_val. + intros; subst; apply ra_project_val. 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 prim_min ra_utils)