Adds an explicit argument to a commutativity rewrite. With iris!971, a different rewrite was performed, which broke the proof.