With nested case rules, if all branches of the inner case rule lead to a
contradiction, it is treated as a contradiction for (the branch
containing the inner case rule) of the outer case rule.