-
Robbert Krebbers authored
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.
4219b955
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.