Painfully slow progress with renaming-Par case of correctness theorem.