Problem with translating terms using SProp

[tabareau]

Definition Has_Leibniz (eq : forall A : Type, A -> A -> Prop) :=
    forall (A : Type) (x : A) (P : A -> SProp), P x -> forall y, eq A x y -> P y.

Definition eq_Has_Leibniz_Prop_elimSP : Has_Leibniz (@eq)
  := @eq_sind.

Parametricity eq.

Fail Parametricity eq_Has_Leibniz_Prop_elimSP.

The command has indeed failed with message: Binder (p₁ : "forall (A : Type) (x : A) (P : A -> SProp), P x -> forall y : A, eq₁ A x y -> P y") has relevance mark set to relevant but was expected to be irrelevant (maybe a bugged tactic).

[ppedrot]

Simpler example:

Require Import Param.

Definition bug := forall (P : SProp), P.

Parametricity bug.