right

The conclusion of the current sequent must be an inductive type or the application of an inductive type with at least two constructors.

Equivalent to constructor 2.

It opens a new sequent for each premise of the second constructor of the inductive type that is the conclusion of the current sequent. For more details, see the constructor tactic.