we proceed by induction on term to prove term

The type of t must be an inductive type and P must be identical to the current conclusion.

It applies the induction principle on t to prove P.

It opens a new sequent for each constructor of the type of t, each with the conclusion P instantiated for the constructor. For the inductive constructors (i.e. if the inductive type is T, constructors with an argument of type T), the conclusion is a logical implication, where the antecedent is the inductive hypothesis for the constructor, and the consequent is P.