we proceed by cases on

we proceed by cases on t to prove th

Synopsis:

we proceed by cases on term to prove term

Pre-condition:

t must inhabitant of an inductive type and th must be the conclusion to be proved by cases.

Action:

It proceeds by cases on t

New sequents to prove:

It opens one new sequent for each constructor of the type of t.