</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the sequent to prove must be an implication
or a universal quantification.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the right introduction rule for implication,
closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding to the hypothesis
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the sequent to prove must be an implication
or a universal quantification.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It applies the right introduction rule for implication,
closing the current sequent.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens a new sequent to prove adding to the hypothesis