finish replCorrect main lemma, modulo some cheats

about type inference, free variables etc.