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
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
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.
- One or more equations did not get rendered due to their size.