fix proof of replCorrectLem, introduce 3 cheats

about the correctness of the type name environment passed to the
compiler