setoid_rewrite: reescribir bajo enlaces con 2 parámetros

Puedo usar la reescritura bajo enlaces con un parámetro

Require Import Setoid.
Require Import Relation_Definitions.
Require Import FunctionalExtensionality.
Parameters f f': nat -> nat.
Parameter wrap: nat -> (nat -> nat) -> nat.
Axiom ff'_eq: forall x, f x = f' x.
Add Parametric Morphism:
 wrap
 with signature (Logic.eq ==> pointwise_relation nat Logic.eq ==> Logic.eq) 
 as wrap_mor.
Proof.
 cbv. intros x f f' H.
 apply functional_extensionality in H.
 rewrite H.
 reflexivity.
Qed.
Lemma test_lemma y:
 wrap y (fun x => f x) = wrap y (fun x => f' x).
 setoid_rewrite ff'_eq.
 reflexivity.
Qed.

Pero no puedo pasar por un caso un poco más complicado, a saber, cuándo wrap: nat -> (nat -> nat -> nat)y f f': nat -> nat -> nat -> nat.

Require Import Setoid.
Require Import Relation_Definitions.
Require Import FunctionalExtensionality.
Parameter f f': nat -> nat -> nat -> nat.
Parameter wrap: nat -> (nat -> nat -> nat) -> nat.
(* Axiom ff'_eq: forall x y z, f x y z = f' x y z. *)
Axiom ff''_eq: forall z, (forall x y, f x y z = f' x y z).
Definition pointwise_relation2:
 forall (A1 A2: Type) {B: Type}, relation B -> relation (A1 -> A2 -> B):= 
 let U:= Type in
 fun (A1 A2 B: U) (R: relation B) (f g: A1 -> A2 -> B) =>
 forall (a1: A1) (a2: A2), R (f a1 a2) (g a1 a2).
Axiom test1: forall (x: nat) (f g: nat -> nat -> nat),
 pointwise_relation2 nat nat Logic.eq f g -> wrap x f = wrap x g.
Add Parametric Morphism:
 wrap with signature 
 (Logic.eq ==> pointwise_relation2 nat nat Logic.eq ==> Logic.eq) 
 as wrap_mor.
Proof. exact test1. Qed.
Lemma test_lemma2 y z:
 wrap y (fun x1 x2 => f x1 x2 z) = wrap y (fun x1 x2 => f' x1 x2 z).
 specialize (ff''_eq z) as feq.
 Fail setoid_rewrite feq.

Una pregunta principalmente es: ¿qué debo usar como relación? No estoy seguro de qué es lo que estoy haciendo mal aquí. ¿Utilizo una relación incorrecta o trato de pasar un argumento incorrecto a setoid_rewrite?

Solución del problema

Puede usar la "relación puntual de una relación puntual" como una relación en funciones binarias:

Require Import Setoid Morphisms.
Parameter f f': nat -> nat -> nat -> nat.
Parameter wrap: nat -> (nat -> nat -> nat) -> nat.
(* Axiom ff'_eq: forall x y z, f x y z = f' x y z. *)
Axiom ff''_eq: forall z, (forall x y, f x y z = f' x y z).
(* The "Add Parametric Morphism" command expands to this instance, which is simpler to write... *)
Axiom test1: Proper (eq ==> pointwise_relation nat (pointwise_relation nat eq) ==> eq) wrap.
Existing Instance test1.
Lemma test_lemma2 y z:
 wrap y (fun x1 x2 => f x1 x2 z) = wrap y (fun x1 x2 => f' x1 x2 z).
Proof.
 specialize (ff''_eq z) as feq.
 setoid_rewrite feq.