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.
Matita Home