New prove_case_eq_thm entrypoint for Prim_rec