Tactic to split if-then-else expressions.

Splits all if-then-else-expressions into multiple goals.
Given a goal of the form `g (if p then x else y)`

, `split_ifs`

will produce
two goals: `p ⊢ g x`

and `¬p ⊢ g y`

.
If there are multiple ite-expressions, then `split_ifs`

will split them all,
starting with a top-most one whose condition does not contain another
ite-expression.
`split_ifs at *`

splits all ite-expressions in all hypotheses as well as the goal.
`split_ifs with h₁ h₂ h₃`

overrides the default names for the hypotheses.

## Equations

- One or more equations did not get rendered due to their size.