They should. This nesting is why `with` exists, but even if `cond` and `case` could test for exhaustiveness (they can't currently, and I don't think that `cond` ever could), `with` would not be able to test for exhaustiveness, since there's always two paths described.