tweak and fix a lemma in replCorrect
update proof of replCorrect_lem