</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>All the terms matched by <span><strong class="command">patt</strong></span> must be
convertible and close in the context of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying a stronger
lemma that is proved using the new generated sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent where the current sequent conclusion
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>All the terms matched by <span><strong class="command">patt</strong></span> must be
convertible and close in the context of the current sequent.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by applying a stronger
lemma that is proved using the new generated sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent where the current sequent conclusion