</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents. The first one has an extra
hypothesis <span><strong class="command">H:P</strong></span>. If <span><strong class="command">H</strong></span> is
omitted, the name of the hypothesis is automatically generated.
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p><span><strong class="command">P</strong></span> must have type <span><strong class="command">Prop</strong></span>.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents. The first one has an extra
hypothesis <span><strong class="command">H:P</strong></span>. If <span><strong class="command">H</strong></span> is
omitted, the name of the hypothesis is automatically generated.