more progress on replCorrect

up to invariant preservation part of the successful declaration case