The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

...is apparently not possible in Coq:

Require Import Arith.

Goal (fun n => n+1) = (fun n => 1+n).
rewrite (plus_comm 1).

  Error: Found no subterm matching "1 + ?4675" in the current goal

I think the reason is that "1+n" can't be abstracted, so "rewrite" 
cannot apply eq_ind_r.
Is this just a technical problem or is there any other way to prove 
this goal?

More generally I'd like to prove
  (fun x => f x) = (fun x => g x)
under the hypthesis
  forall x, f x = g x