</p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The conclusion of the current proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by transitivity of the equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents <span><strong class="command">l=t</strong></span> and
<span><strong class="command">t=r</strong></span> where <span><strong class="command">l</strong></span> and <span><strong class="command">r</strong></span> are the left and right hand side of the equality in the conclusion of
the current sequent to prove.</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 proof must be an equality.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It closes the current sequent by transitivity of the equality.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens two new sequents <span><strong class="command">l=t</strong></span> and
<span><strong class="command">t=r</strong></span> where <span><strong class="command">l</strong></span> and <span><strong class="command">r</strong></span> are the left and right hand side of the equality in the conclusion of
the current sequent to prove.</p></dd></dl></div><p>