Record, Proof irrelevance, and John Major's equality

Question

Suppose I have the following type of record:

Record R (A : Type) (P : A -> Prop) := {val : A; prop : P val}.

To prove that two such records are equal, it is sufficient (by proof irrelevance) to prove that their fields val are equal:

Goal forall A P (r1 r2 : R A P), val _ _ r1 = val _ _ r2 -> r1 = r2.
destruct r1, r2.
simpl.
intro H.
revert prop0.
rewrite H.
intros.
f_equal.
apply proof_irrelevance.
Qed.

Is a similar goal provable (possibly relying on a safe axiom) in the case of John Major's equality? Here is my failed attempt:

Goal forall A1 A2 P1 P2 (r1 : R A1 P1) (r2 : R A2 P2),
JMeq (val _ _ r1) (val _ _ r2) -> JMeq r1 r2.
destruct r1, r2.
simpl.
intro H.
revert prop0.
Fail rewrite H.

Answer 1

No, it isn't (short of assuming False, of course). The problem is that JMeq implies that the types are equal:

Require Import Coq.Logic.JMeq.

Record R (A : Type) (P : A -> Prop) := {val : A; prop : P val}.

Axiom contra : forall A1 A2 P1 P2 (r1 : R A1 P1) (r2 : R A2 P2),
JMeq (val _ _ r1) (val _ _ r2) -> JMeq r1 r2.

Goal False.
assert (H1 := contra nat nat (fun n => True) (eq 0) (Build_R _ _ 0 I) (Build_R _ _ 0 eq_refl)).
assert (H2 : R nat (fun n => True) = R nat (eq 0) :> Type).
{ now destruct H1. }
assert (H3 : forall r1 r2 : R nat (fun _ => True), r1 = r2).
{ rewrite H2. intros [n1 p1] [n2 p2].
  now destruct p1; destruct p2. }
specialize (H3 (Build_R _ _ 0 I) (Build_R _ _ 1 I)).
discriminate.
Qed.