TY  - RPRT
TI  - Generating induction principles and subterm relations for inductive types using MetaCoq
AU  - Bohdan Liesnikov
AU  - Marcel Ullrich
AU  - Yannick Forster
PY  - 2020
UR  - https://arxiv.org/abs/2006.15135
ID  - 2006.15135
ER  -