split
The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least one constructor.
Equivalent to constructor 1.
It opens a new sequent for each premise of the first constructor of the inductive type that is the conclusion of the current sequent. For more details, see the constructor tactic.