<command>T<subscript>i</subscript></command> that is not
instantiated by unification. <command>T<subscript>i</subscript></command> is
the conclusion of the <command>i</command>-th new sequent to
<command>T<subscript>i</subscript></command> that is not
instantiated by unification. <command>T<subscript>i</subscript></command> is
the conclusion of the <command>i</command>-th new sequent to
proof is in the search space that is pruned away. Pruning is
controlled by <command>d</command> and <command>w</command>.
Moreover, only lemmas whose type signature is a subset of the
proof is in the search space that is pruned away. Pruning is
controlled by <command>d</command> and <command>w</command>.
Moreover, only lemmas whose type signature is a subset of the
rewriting steps (unless <command>paramodulation</command> is
omitted), hypothesis and lemmas in the library.</para>
</listitem>
rewriting steps (unless <command>paramodulation</command> is
omitted), hypothesis and lemmas in the library.</para>
</listitem>
sequent context. Thus the definition becomes an hypothesis.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
sequent context. Thus the definition becomes an hypothesis.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
<command>patt</command> with the new term <command>t</command>.
For each subterm matched by the pattern, <command>t</command> is
disambiguated in the context of the subterm.</para>
<command>patt</command> with the new term <command>t</command>.
For each subterm matched by the pattern, <command>t</command> is
disambiguated in the context of the subterm.</para>
an inductive type or the application of an inductive type with
at least <command>n</command> constructors.</para>
</listitem>
an inductive type or the application of an inductive type with
at least <command>n</command> constructors.</para>
</listitem>
that can not be inferred by unification. For more details,
see the <command>apply</command> tactic.</para>
</listitem>
that can not be inferred by unification. For more details,
see the <command>apply</command> tactic.</para>
</listitem>
hypothesis <command>H:P</command>. If <command>H</command> is
omitted, the name of the hypothesis is automatically generated.
The second sequent has conclusion <command>P</command> and
hypothesis <command>H:P</command>. If <command>H</command> is
omitted, the name of the hypothesis is automatically generated.
The second sequent has conclusion <command>P</command> and
the new hypotheses are picked by <command>hyps</command>, if
provided. If hyps specifies also a number of hypotheses that
is less than the number of new hypotheses for a new sequent,
the new hypotheses are picked by <command>hyps</command>, if
provided. If hyps specifies also a number of hypotheses that
is less than the number of new hypotheses for a new sequent,
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
<command>patt</command>. In the context of each matched subterm
it disambiguates the term <command>t</command> and reduces it
to its <command>red</command> normal form; then it replaces with
<command>patt</command>. In the context of each matched subterm
it disambiguates the term <command>t</command> and reduces it
to its <command>red</command> normal form; then it replaces with
inequation over real numbers taken from standard library of
Coq. Moreover the inequations in the hypotheses must imply the
inequation in the conclusion of the current sequent.</para>
inequation over real numbers taken from standard library of
Coq. Moreover the inequations in the hypotheses must imply the
inequation in the conclusion of the current sequent.</para>
<command>G</command> is generalized to
<command>∀x.G{x/t}</command> where <command>{x/t}</command>
is a notation for the replacement with <command>x</command> of all
<command>G</command> is generalized to
<command>∀x.G{x/t}</command> where <command>{x/t}</command>
is a notation for the replacement with <command>x</command> of all
with the additional hypotheses
<command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
</listitem>
with the additional hypotheses
<command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
</listitem>
the antecedent of the implication and setting the conclusion
to the consequent of the implicaiton. The name of the new
hypothesis is <command>H</command> if provided; otherwise it
the antecedent of the implication and setting the conclusion
to the consequent of the implicaiton. The name of the new
hypothesis is <command>H</command> if provided; otherwise it
implication, closing the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
implication, closing the current sequent.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
hypotheses equal to the number of new hypotheses requested.
If the user does not request a precise number of new hypotheses,
it adds as many hypotheses as possible.
hypotheses equal to the number of new hypotheses requested.
If the user does not request a precise number of new hypotheses,
it adds as many hypotheses as possible.
definition of the type of <command>t</command>. With respect to
a simple elimination, each new sequent has additional hypotheses
that states the equalities of the "right parameters"
definition of the type of <command>t</command>. With respect to
a simple elimination, each new sequent has additional hypotheses
that states the equalities of the "right parameters"
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
<command>patt</command> with the new term <command>t</command>.
For each subterm matched by the pattern, <command>t</command> is
disambiguated in the context of the subterm.</para>
<command>patt</command> with the new term <command>t</command>.
For each subterm matched by the pattern, <command>t</command> is
disambiguated in the context of the subterm.</para>
for all the occurrences of the
left hand side of the equality that <command>p</command> proves
(resp. the right hand side if <command>dir</command> is
for all the occurrences of the
left hand side of the equality that <command>p</command> proves
(resp. the right hand side if <command>dir</command> is
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
equality over Coq's real numbers that can be proved using
the ring properties of the real numbers only.</para>
</listitem>
equality over Coq's real numbers that can be proved using
the ring properties of the real numbers only.</para>
</listitem>
means of computation (i.e. this is a reflexive tactic, implemented
exploiting the "two level reasoning" technique).</para>
</listitem>
means of computation (i.e. this is a reflexive tactic, implemented
exploiting the "two level reasoning" technique).</para>
</listitem>
with other convertible terms that are supposed to be simpler.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
with other convertible terms that are supposed to be simpler.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>New sequents to prove:</term>
<listitem>
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the <command>constructor</command> tactic.</para>
</listitem>
<command>t=r</command> where <command>l</command> and <command>r</command> are the left and right hand side of the equality in the conclusion of
the current sequent to prove.</para>
</listitem>
<command>t=r</command> where <command>l</command> and <command>r</command> are the left and right hand side of the equality in the conclusion of
the current sequent to prove.</para>
</listitem>
(possibly applied to arguments) in the subterms matched by
<command>patt</command>. Then it δ-expands each occurrence,
also performing β-reduction of the obtained term. If
(possibly applied to arguments) in the subterms matched by
<command>patt</command>. Then it δ-expands each occurrence,
also performing β-reduction of the obtained term. If