Move some cheats

Uncommented some old theorems that prove the cheats in replCorrect'_lem.
But the old theorems are currently cheated themselves pending fixing.