M. Sozeau, “A New Look at Generalized Rewriting in Type Theory”, JFR, vol. 2, no. 1, pp. 41–62, Jan. 2009.