open the branching tactical \verb+[+. Then you can interact with the system
reaching a proof of the first case, without having to specify the whole
branching tactical. When you have proved all the induction cases, you close
open the branching tactical \verb+[+. Then you can interact with the system
reaching a proof of the first case, without having to specify the whole
branching tactical. When you have proved all the induction cases, you close