Assia Mahboubi, Enrico Tassi: Canonical Structures for the Working Coq User. ITP 2013: 19-34