- <entry>[<emphasis role="bold">obtain</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> | <emphasis role="bold">conclude</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>] <emphasis role="bold">=</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">by</emphasis> [ <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">_</emphasis> [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">)</emphasis>]] [<emphasis role="bold">done</emphasis>]</entry>
+ <entry><link linkend="tac_we need to prove"><emphasis role="bold">we need to prove</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
+ [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
+ <emphasis role="bold">)</emphasis>]
+ [ <emphasis role="bold">or equivalently</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>]</entry>