+ <titleabbrev>id</titleabbrev>
+ <para><userinput>id </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">id</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>This identity tactic does nothing without failing.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_intro">
+ <title>intro</title>
+ <titleabbrev>intro</titleabbrev>
+ <para><userinput>intro H</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">intro</emphasis> [&id;]</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the sequent to prove must be an implication
+ or a universal quantification.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It applies the right introduction rule for implication,
+ closing the current sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent to prove adding to the hypothesis
+ 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
+ is automatically generated.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_intros">
+ <title>intros</title>
+ <titleabbrev>intros</titleabbrev>
+ <para><userinput>intros hyps</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">intros</emphasis> &intros-spec;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>If <command>hyps</command> specifies a number of hypotheses
+ to introduce, then the conclusion of the current sequent must
+ be formed by at least that number of imbricated implications
+ or universal quantifications.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It applies several times the right introduction rule for
+ implication, closing the current sequent.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent to prove adding a number of new
+ 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.
+ The name of each new hypothesis is either popped from the
+ user provided list of names, or it is automatically generated when
+ the list is (or becomes) empty.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_inversion">
+ <title>inversion</title>
+ <titleabbrev>inversion</titleabbrev>
+ <para><userinput>inversion t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">inversion</emphasis> &sterm;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The type of the term <command>t</command> must be an inductive
+ type or the application of an inductive type.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It proceeds by cases on <command>t</command> paying attention
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent to prove for each case in the
+ 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"
+ of the inductive type with terms originally present in the
+ sequent to prove.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_lapply">
+ <title>lapply</title>
+ <titleabbrev>lapply</titleabbrev>
+ <para><userinput>
+ lapply linear depth=d t
+ to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
+ </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>
+ <emphasis role="bold">lapply</emphasis>
+ [<emphasis role="bold">linear</emphasis>]
+ [<emphasis role="bold">depth=</emphasis>&nat;]
+ &sterm;
+ [<emphasis role="bold">to</emphasis>
+ &sterm;
+ [<emphasis role="bold">,</emphasis>&sterm;…]
+ ]
+ [<emphasis role="bold">as</emphasis> &id;]
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>
+ <command>t</command> must have at least <command>d</command>
+ independent premises and <command>n</command> must not be
+ greater than <command>d</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>
+ Invokes <command>letin H ≝ (t ? ... ?)</command>
+ with enough <command>?</command>'s to reach the
+ <command>d</command>-th independent premise of
+ <command>t</command>
+ (<command>d</command> is maximum if unspecified).
+ Then istantiates (by <command>apply</command>) with
+ t<subscript>1</subscript>, ..., t<subscript>n</subscript>
+ the <command>?</command>'s corresponding to the first
+ <command>n</command> independent premises of
+ <command>t</command>.
+ Usually the other <command>?</command>'s preceding the
+ <command>n</command>-th independent premise of
+ <command>t</command> are istantiated as a consequence.
+ If the <command>linear</command> flag is specified and if
+ <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
+ are (applications of) premises in the current context, they are
+ <command>clear</command>ed.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>
+ The ones opened by the tactics <command>lapply</command> invokes.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_left">
+ <title>left</title>
+ <titleabbrev>left</titleabbrev>
+ <para><userinput>left </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">left</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 1</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_letin">
+ <title>letin</title>
+ <titleabbrev>letin</titleabbrev>
+ <para><userinput>letin x ≝ t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">letin</emphasis> &id; <emphasis role="bold">≝</emphasis> &sterm;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It adds to the context of the current sequent to prove a new
+ definition <command>x ≝ t</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_normalize">
+ <title>normalize</title>
+ <titleabbrev>normalize</titleabbrev>
+ <para><userinput>normalize patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">normalize</emphasis> &pattern;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with their βδιζ-normal form.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_reflexivity">
+ <title>reflexivity</title>
+ <titleabbrev>reflexivity</titleabbrev>
+ <para><userinput>reflexivity </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">reflexivity</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ <command>t=t</command> for some term <command>t</command></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent by reflexivity
+ of equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_replace">
+ <title>replace</title>
+ <titleabbrev>change</titleabbrev>
+ <para><userinput>change patt with t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">replace</emphasis> &pattern; <emphasis role="bold">with</emphasis> &sterm;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces the subterms of the current sequent matched by
+ <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>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>For each matched term <command>t'</command> it opens
+ a new sequent to prove whose conclusion is
+ <command>t'=t</command>.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_rewrite">
+ <title>rewrite</title>
+ <titleabbrev>rewrite</titleabbrev>
+ <para><userinput>rewrite dir p patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">rewrite</emphasis> [<emphasis role="bold"><</emphasis>|<emphasis role="bold">></emphasis>] &sterm; &pattern;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para><command>p</command> must be the proof of an equality,
+ possibly under some hypotheses.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It looks in every term matched by <command>patt</command>
+ 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
+ <command><</command>). Every occurence found is replaced with
+ the opposite side of the equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens one new sequent for each hypothesis of the
+ equality proved by <command>p</command> that is not closed
+ by unification.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_right">
+ <title>right</title>
+ <titleabbrev>right</titleabbrev>
+ <para><userinput>right </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">right</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least two constructors.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 2</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the second
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_ring">
+ <title>ring</title>
+ <titleabbrev>ring</titleabbrev>
+ <para><userinput>ring </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">ring</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be an
+ equality over Coq's real numbers that can be proved using
+ the ring properties of the real numbers only.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent veryfying the equality by
+ means of computation (i.e. this is a reflexive tactic, implemented
+ exploiting the "two level reasoning" technique).</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_simplify">
+ <title>simplify</title>
+ <titleabbrev>simplify</titleabbrev>
+ <para><userinput>simplify patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">simplify</emphasis> &pattern;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with other convertible terms that are supposed to be simpler.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_split">
+ <title>split</title>
+ <titleabbrev>split</titleabbrev>
+ <para><userinput>split </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">split</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least one constructor.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>Equivalent to <command>constructor 1</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the <command>constructor</command> tactic.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_subst">
+ <title>subst</title>
+ <titleabbrev>subst</titleabbrev>
+ <para><userinput>subst</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">subst</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem><para>
+ None.
+ </para></listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem><para>
+ For each premise of the form
+ <command>H: x = t</command> or <command>H: t = x</command>
+ where <command>x</command> is a local variable and
+ <command>t</command> does not depend on <command>x</command>,
+ the tactic rewrites <command>H</command> wherever
+ <command>x</command> appears clearing <command>H</command> and
+ <command>x</command> afterwards.
+ </para></listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem><para>
+ The one opened by the applied tactics.
+ </para></listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_symmetry">
+ <title>symmetry</title>
+ <titleabbrev>symmetry</titleabbrev>
+ <para>The tactic <command>symmetry</command> </para>
+ <para><userinput>symmetry </userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">symmetry</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be an equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It swaps the two sides of the equalityusing the symmetric
+ property.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_transitivity">
+ <title>transitivity</title>
+ <titleabbrev>transitivity</titleabbrev>
+ <para><userinput>transitivity t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">transitivity</emphasis> &sterm;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>The conclusion of the current proof must be an equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It closes the current sequent by transitivity of the equality.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>It opens two new sequents <command>l=t</command> and
+ <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>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_unfold">
+ <title>unfold</title>
+ <titleabbrev>unfold</titleabbrev>
+ <para><userinput>unfold t patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">unfold</emphasis> [&sterm;] &pattern;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It finds all the occurrences of <command>t</command>
+ (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
+ <command>t</command> is omitted it defaults to each
+ subterm matched by <command>patt</command>.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+ <sect1 id="tac_whd">
+ <title>whd</title>
+ <titleabbrev>whd</titleabbrev>
+ <para><userinput>whd patt</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">whd</emphasis> &pattern;</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It replaces all the terms matched by <command>patt</command>
+ with their βδιζ-weak-head normal form.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>