Removed more cheats.

There is one remaining cheat, and the cheated lemma will need a stronger
precondition about data constructor uniqueness to be true.