Gilles Barthe, Olivier Pons, Type Isomorphisms and Proof Reuse in Dependent Type Theory, in Foundations of Software Science and Computation Structures. FoSSaCS 2001, Lecture Notes in Computer Science 2030, Springer (2001) [doi:10.1007/3-540-45315-6_4]