About symbols for case analysis

[jaewooklee93]

For this week's assignment, I use more than three levels of case analysis and I'm running out of symbols. For the depth<4, of course, I used -, +, *, but after that what can I use? I know { works as well, but they need to be closed by }, so it is cumbersome to use and not pretty, too...

[jaewooklee93]

Well, if I use { as outermost case, I don't need to close them for so many times.

[jeehoonkang]

If you enclose script by { }, you can use - + * once more. I structure proof like this:

- ...
  + ...
    * ...
      { ...
        - ...
      }

[jaewooklee93]

But if I have to write many cases with depth 4 (not 5), Is the only way the following?

- ...
  + ...
    * ...
      { ...
      }
      { ...
      }
      { ...
      }
      { ...
      }
      ...

[jeehoonkang]

Unfortunately, yes..

but that deep depth smells the need of sublemmas, said the Coq developers..