Neil Ghani: Eta-Expansions in Dependent Type Theory - The Calculus of Constructions. TLCA 1997: 164-180