</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least two constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 2</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the second
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least two constructors.</p></dd><dt><span class="term">Action:</span></dt><dd><p>Equivalent to <span><strong class="command">constructor 2</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent for each premise of the second