cases term pattern [([id]…)]

t must inhabit an inductive type

It proceed by cases on t. The new generated hypothesis in each branch are named according to hyps. The elimintation predicate is restricted by pattern. In particular, if some hypothesis is listed in pattern, the hypothesis is generalized and cleared before proceeding by cases on t. Currently, we only support patterns of the form H₁ … H_n ⊢ %. This limitation will be lifted in the future.

One new sequent for each constructor of the type of t. Each sequent has a new hypothesis for each argument of the constructor.