* [as id]

The current conclusion must be of the form T → G where I is an inductive type applied to its arguments, if any.

It introduces a new hypothesis H of type T. Then it proceeds by cases over H. Finally, if the name H is not specified, it clears the new hypothesis from all contexts.

The ones generated by case analysis.