Fix proof broken by db871b5d9d

In particular, its making of x IN (\y. P y) = P x into an automatic
rewrite caused problems. The fixed proof doesn’t depend on this one
way or the other and is shorter to boot.