</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
<span><strong class="command">t=t</strong></span> for some term <span><strong class="command">t</strong></span></p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by reflexivity
of equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>
</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current sequent must be
<span><strong class="command">t=t</strong></span> for some term <span><strong class="command">t</strong></span></p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by reflexivity
of equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>None.</p></dd></dl></div><p>