Include Richard Eisenberg's suggestion for decidable type equality (functionality not complete yet).
Eliminate unneeded imports.