+ <sect1 id="tac_bytermweproved">
+ <title>we proved</title>
+ <titleabbrev>we proved</titleabbrev>
+ <para><userinput>justification we proved T [(id)]</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>&justification; <emphasis role="bold">we proved</emphasis> &term;
+ [<emphasis role="bold">(</emphasis> &id;
+ <emphasis role="bold">)</emphasis>]
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>
+ None.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>
+ If <command>id</command> is supplied, a logical cut on <command>T</command> is made. Otherwise, if <command>T</command> is identical to the current conclusion, it allows the user to start a chain of reductions on the conclusion with the tactic <emphasis role="bold">that is equivalent to</emphasis>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>
+ If <command>id</command> is supplied, a new sequent with <command>T</command> as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis <command>T</command> is added to the context, with name <command>id</command>.
+ If <command>id</command> is not supplied, no new sequents are opened.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+
+ <sect1 id="tac_existselim">
+ <title>let such that</title>
+ <titleabbrev>let such that</titleabbrev>
+ <para><userinput>justification let x:T such that P (H)</userinput>
+ </para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>&justification; <emphasis role="bold">let</emphasis> &id;
+ <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term;
+ <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>
+ None.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>
+ It applies the left introduction rule of the existential quantifier on the formula <command>∃ x. P(x)</command> (in Natural Deduction this corresponds to the elimination rule for the quantifier).
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>A new sequent with <command>∃ x. P(x)</command> as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses <command>x : T</command> and <command>H : P</command> are added to the context.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>