Then it closes the current sequent by applying
<command>t</command> to <command>n</command>
implicit arguments (that become new sequents).
Then it closes the current sequent by applying
<command>t</command> to <command>n</command>
implicit arguments (that become new sequents).
<listitem>
<para>None, but the tactic may fail finding a proof if every
proof is in the search space that is pruned away. Pruning is
<listitem>
<para>None, but the tactic may fail finding a proof if every
proof is in the search space that is pruned away. Pruning is
Moreover, only lemmas whose type signature is a subset of the
signature of the current sequent are considered. The signature of
Moreover, only lemmas whose type signature is a subset of the
signature of the current sequent are considered. The signature of