replace rewrite with cong where feasible