proposition: Fact ra_proj_tot n p : total [| @ra_proj n p |].
proof: Proof. intros v; exists (vec_pos v p); simpl; red; auto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec