Sozeau, M. “A New Look at Generalized Rewriting in Type Theory”. Journal of Formalized Reasoning, vol. 2, no. 1, Jan. 2009, pp. 41-62, doi:10.6092/issn.1972-5787/1574.