- <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><link linkend="grammar.autoparams">auto_params</link></emphasis> | <emphasis role="bold">exact</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">proof</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>