constructor

%n {args}

Synopsis:

% [nat] [{sterm}]

Pre-conditions:

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

Action:

It applies the n-th constructor of the inductive type of the conclusion of the current sequent to the arguments args. If n is omitted, it defaults to 1.

New sequents to prove:

It opens a new sequent for each premise of the constructor that can not be inferred by unification. For more details, see the apply tactic.