A Rewriting Strategy to Verify Observational Congruence