Implement and document a new prove_case_rand_thm function in Prim_rec.

This will be the basis for a general tool that moves case-constants up
within a term and then eliminates them, subsuming, for example, the
functionality in boolSimps.COND_elim_ss, which does this but only for
the boolean case-constant (aka if-then-else).