Goal forall n, n+n=0->0=n+n.
intros.

(* This used to fail in 8.0pl1 *)
set n in * |-.