Sozeau, M. A New Look at Generalized Rewriting in Type Theory. JFR 2009, 2, 41-62.