we proceed by cases on t to prove P
The type of t must be an inductive type and P must be identical to the current conclusion.
It proceeds by case-analysis on t
It opens one new sequent for each constructor of the type of t, each with the conclusion P instantiated for the constructor.