The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to prove the following goal without functional extensionality (using something like setoid_rewrite)?

Require Import Setoid.

Goal forall f g a : Type -> Type, (forall x, f x = g x) -> (fun x => a (f x)) = (fun x => a (g x)).

  intros.

  setoid_rewrite H.

Also, why do I get ' Warning: Invalid character '-' in identifier "_UNBOUND_REL_-1". ' in the following?

Require Import Setoid.

Goal forall f g : Type -> Type, (forall x, f x = g x) -> (fun (a : Type -> Type) x => a (f x)) = (fun (a : Type -> Type) x => a (g x)).

  intros.

  setoid_rewrite H.

Thanks.

-Jason