we proceed by cases on term to prove term

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.