cases t pattern


cases term pattern


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 H1 … Hn ⊢ %. This limitation will be lifted in the future.

New sequents to prove:

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