It should be easy to rewrite under binders with function extensionality

[JasonGross]

Version

8.9+alpha

Description of the problem

I would like to see a standard library file which depends on the axiom of function extensionality and registers the typeclass instances required to rewrite under binders with eq. I think the relevant instance might be subrelation R eq -> subrelation (pointwise_relation _ R) eq, but I'm not 100% sure.

cc @mattam82

[SkySkimmer]

Require Import Setoid Morphisms FunctionalExtensionality.

Local Instance foo'
  : forall A B C f, Proper (pointwise_relation A (@eq B) ==> (@eq C)) f.
Proof.
  cbv. intros.
  f_equal.
  apply functional_extensionality.
  exact H.
Qed.

Lemma bar (P:(nat -> nat) -> Prop) : P (fun x => x + 0) -> P (fun x => x).
Proof.
  setoid_rewrite <-plus_n_O.

seems to work