Case splits on a term t that features in the goal as case t of ...,
and then performs some simplification.
BasicProvers.CASE_TAC first calls BasicProvers.PURE_CASE_TAC, which
searches the goal for an instance of case t of ... and performs a
BasicProvers.Cases_on `t`. If this succeeds, it then simplifies the
goal using definitions of case constants, plus distinctness and
injectivity theorems for datatypes.
When there are multiple case constants in the goal, it can be very
convenient to execute the tactic REPEAT CASE_TAC. bossLib.CASE_TAC
is the same as BasicProvers.CASE_TAC.
BasicProvers.CASE_TAC fails precisely when BasicProvers.PURE_CASE_TAC