<term>Pre-conditions:</term>
<listitem>
<para><command>t</command> must have type
- <command>T<subscript>1</subscript> → ... →
+ <command>T<subscript>1</subscript> → … →
T<subscript>n</subscript> → G</command>
where <command>G</command> can be unified with the conclusion
of the current sequent.</para>