Like force but immediately splits the top-level goal on the hypothesis

`force`, which has similar
special treatment in hypotheses of rules for the same rule-classes as
for `rewrite`, `linear`, `type-prescription`, `definition`, `meta` (actually in
that case, the result of evaluating the hypothesis metafunction call), and
`forward-chaining`.

When a hypothesis of a conditional rule (of one of the classes listed
above) has the form

For example, given the rule

(defthm p1->p2 (implies (case-split (p1 x)) (p2 x)))

then an attempt to prove

(implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:

(IMPLIES (AND (NOT (P1 (CAR X))) (P3 X)) (P2 (CAR X))).

Unlike `force`,

The special ``split'' treatment of `if` term present in the goal
being simplified. Since `and` terms and `or` terms are merely
abbreviations for `if` terms, they also prevent splitting. Note that
`if` terms are ultimately eliminated using the ordinary flow of the
proof (but see set-case-split-limitations), so

When in the interactive proof-builder,

**Function: **

(defun case-split (x) (declare (xargs :guard t)) x)