+ 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.