exists

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.