<term>Pre-conditions:</term>
<listitem>
<para><command>t</command> must have type
- <command>T<subscript>1</subscript> → ... →
+ <command>T<subscript>1</subscript> → … →
T<subscript>n</subscript> → G</command>
where <command>G</command> can be unified with the conclusion
of the current sequent.</para>
<title>cases</title>
<titleabbrev>cases</titleabbrev>
<para><userinput>
- cases t hyps
+ cases t pattern hyps
</userinput></para>
<para>
<variablelist>
<listitem>
<para>
<emphasis role="bold">cases</emphasis>
- &term; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+ &term; &pattern; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
</para>
</listitem>
</varlistentry>
It proceed by cases on <command>t</command>. The new generated
hypothesis in each branch are named according to
<command>hyps</command>.
+ The elimintation predicate is restricted by
+ <command>pattern</command>. In particular, if some hypothesis
+ is listed in <command>pattern</command>, the hypothesis is
+ generalized and cleared before proceeding by cases on
+ <command>t</command>. Currently, we only support patterns of the
+ form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
</para>
</listitem>
</varlistentry>