</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">K t<sub>1</sub> ... t<sub>n</sub> = K t'<sub>1</sub> ... t'<sub>n</sub></strong></span> where both argument lists are empty if
<span><strong class="command">K</strong></span> takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It derives new hypotheses by injectivity of
<span><strong class="command">K</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>The new sequent to prove is equal to the current sequent
</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">K t<sub>1</sub> ... t<sub>n</sub> = K t'<sub>1</sub> ... t'<sub>n</sub></strong></span> where both argument lists are empty if
<span><strong class="command">K</strong></span> takes no arguments.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It derives new hypotheses by injectivity of
<span><strong class="command">K</strong></span>.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>The new sequent to prove is equal to the current sequent