+ <sect1 id="tac_thatisequivalentto">
+ <title>that is equivalent to</title>
+ <titleabbrev>that is equivalent to</titleabbrev>
+ <para><userinput>that is equivalent to t</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para>
+ <emphasis role="bold">that is equivalent to</emphasis> &term;
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>
+ The user must have applied one of the following tactics immediately before applying this tactic: <emphasis role="bold">assume</emphasis>, <emphasis role="bold">suppose</emphasis>, <emphasis role="bold">we need to prove</emphasis>, <emphasis role="bold">by just we proved</emphasis>,<emphasis role="bold">the thesis becomes</emphasis>, <emphasis role="bold">that is equivalent to</emphasis>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>
+ If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term <command>t</command> is beta-equivalent to the term <command>t1</command> on which this tactic is working (i.e. they can be reduced to a common term), <command>t1</command> is changed with <command>t</command>.
+
+ If the tactic that was applied before this tactic was <emphasis role="bold">that is equivalent to</emphasis>, and that tactic was working on a term <command>t1</command>, this tactic keeps working on <command>t1</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>
+ If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to <command>t</command> is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with <command>t</command>.
+ </para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_thesisbecomes">
+ <title>the thesis becomes</title>
+ <titleabbrev>the thesis becomes</titleabbrev>
+ <para><userinput>the thesis becomes P</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-condition:</term>
+ <listitem>
+ <para>The provided term <command>P</command> must be identical to the current conclusion.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem>
+ <para>It allows the user to start a chain of reductions on the conclusion with the tactic <emphasis role="bold">that is equivalent to</emphasis>, after stating the current conclusion.</para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequent to prove:</term>
+ <listitem>
+ <para>None.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+
+ <sect1 id="tac_weneedtoprove">
+ <title>we need to prove</title>
+ <titleabbrev>we need to prove</titleabbrev>
+ <para><userinput>we need to prove T [(H)]</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">we need to prove</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 provided, it applies a logical cut on <command>T</command>. Otherwise, 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 sequents to prove:</term>
+ <listitem>
+ <para>If <command>id</command> is supplied, a new sequent with <command>T</command> as the conclusion is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with <command>H:T</command> added to the hypotheses.</para>
+ </listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
+