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.