citp csp

:csp { eq [ <label-exp>] <term> = <term> . ...}

Applies case splitting after a set of equations. Each of these equations creates one new sub-goal with the equation added.

The system does not check whether given set of equations exhausts all possible values.

Not discharged sub-goals will remain in the reduced form.

Related: :csp-, citp