Сигнатура морфизма для зависимо типизированных векторов в coq

Я хочу иметь возможность переписывать термины внутри предиката P, переданного Coq.Vectors.Vector.Forall.

Первая попытка не работает из-за отсутствия квантификации над n.

From Coq Require Import Vector Morphisms Setoid.

Parameter D : Type.
Parameter R : relation D.

Fail Add Parametric Morphism : (@Forall D)
    with signature (R ==> iff) ==> Forall2 R ==> iff
     as morph1.
(* The term "Forall" has type "(D -> Prop) -> forall n : nat, t D n -> Prop"
   while it is expected to have type "(D -> Prop) -> t D ?n -> Prop". *)

Мне удалось доказать следующее, с фиксированным размером вектора, но на практике это бесполезно.

Add Parametric Morphism n : (fun P => @Vector.Forall D P n)
    with signature (R ==> iff) ==> Forall2 R ==> iff
      as morph2.
Proof.
  intros P Q Hpq v1 v2 Hr.
  rewrite 2 Forall_nth_order.
  rewrite Forall2_nth_order in Hr.
  split; intros Hf i Hi; eapply Hpq; eauto.
  Unshelve.
  all: assumption.
Qed.

Какой может быть правильная подпись для morph1?