Ahrens, Benedikt, and Julianna Zsido. 2011. “Initial Semantics for Higher-Order Typed Syntax in Coq”. Journal of Formalized Reasoning 4 (1):25-69. https://doi.org/10.6092/issn.1972-5787/2066.