- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para><command>conclude</command> can be used only if the current
- sequent is stating an equality. The left hand side must be omitted
- in an equality chain.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>Starts or continues an equality chain. If the chain starts
- with <command>obtain H</command> a new subproof named
- <command>H</command> is started.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequent to prove:</term>
- <listitem>
- <para>If the chain starts
- with <command>obtain H</command> a nre sequent for
- <command>t2 = ?</command> is opened.
- </para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
-
- <sect1 id="tac_suppose">
- <title>suppose</title>
- <titleabbrev>suppose</titleabbrev>
- <para><userinput>suppose t1 (x) that is equivalent to t2</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id;
- <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis> &term; ]</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-condition:</term>
- <listitem>
- <para>The conclusion of the current proof must be
- <command>∀x:T.P</command> or
- <command>T→P</command> where <command>T</command> is
- a proposition (i.e. <command>T</command> has type
- <command>Prop</command> or <command>CProp</command>).</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>