we proceed by induction on
we proceed by induction on t to prove th
- Synopsis:
we proceed by induction on term to prove term
- Pre-condition:
t must inhabitant of an inductive type and
th must be the conclusion to be proved by induction.
- Action:
It proceed by induction on t.
- New sequents to prove:
It opens one new sequent for each constructor of the
type of t.
Matita Home