thoughts about an invariant for proving replCorrect_lem

previously the statement was on universally quantified repl_state and
repl_fun_state, with no connection between them; that probably isn't
going to be true.