@misc{indiciae9da379570628, title = {Generating induction principles and subterm relations for inductive types using MetaCoq}, author = {Bohdan Liesnikov and Marcel Ullrich and Yannick Forster}, year = {2020}, url = {https://arxiv.org/abs/2006.15135}, note = {Source identifier: 2006.15135} }