Require Import Coq.Setoids.Setoid.
Require Import VST.msl.Extensionality.

(******************************************

Copied From Coq.Logic.JMeq.

No longer involving JMeq_eq, which is potentially inconsistenty with homotopy
type theory.

TODO: let reflexivity, symmetry and transitivity work again.

******************************************)

Definition JMeq {A:Type} (x:A) {B:Type} (y: B): Prop :=
  {H: @eq Type A B | @eq_rect Type A (fun T: Type => T) x B H = y}.

Lemma JMeq_refl: forall {A: Type} (x: A), JMeq x x.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A x A x *)
  exists eq_refl.
(* Goal: @eq A (f A a a') (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) a') *)
  rewrite <- eq_rect_eq.
(* Goal: @eq C (f A b) (f A b) *)
  auto.
Qed.
Hint Resolve JMeq_refl.

Lemma JMeq_sym : forall {A: Type} {B:Type} {x:A} {y:B}, JMeq x y -> JMeq y x.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq B y A x *)
  destruct H as [?H ?H].
(* Goal: @JMeq B y A x *)
  exists (eq_sym H).
(* Goal: @eq A (@eq_rect Type B (fun T : Type => T) y A (@eq_sym Type A B H)) x *)
  rewrite <- H0.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) (f A a a') A (@eq_refl Type A)) (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) (@eq_rect Type A (fun T : Type => T) a' A (@eq_refl Type A))) *)
  simpl.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.
Hint Immediate JMeq_sym.

Lemma JMeq_trans :
 forall {A: Type} {B: Type} {C:Type} {x:A} {y:B} {z:C}, JMeq x y -> JMeq y z -> JMeq x z.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  destruct H as [?H ?H], H0 as [?H ?H].
(* Goal: @JMeq A x C z *)
  exists (eq_trans H H0).
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) x A (@eq_trans Type A A A (@eq_refl Type A) (@eq_refl Type A))) z *)
  rewrite <- H2, <- H1.
(* Goal: @eq (F B) (@eq_rect_r T B F (@eq_rect_r T B F x B (@eq_sym T B B (@eq_refl T B))) B (@eq_refl T B)) x *)
  reflexivity.
Qed.

Lemma JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @eq C (f A a) (f A b) *)
  rewrite <- eq_rect_eq in e.
(* Goal: @eq A x y *)
  exact e.
Qed.

Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
  P x -> forall y, JMeq x y -> P y.
Proof.
(* Goal: forall (A : Type) (x : A) (P : forall _ : A, Prop) (_ : P x) (y : A) (_ : @JMeq A x A y), P y *)
intros A x P H y H'.
(* Goal: P y *)
inversion H'.
(* Goal: @JMeq (F y) (@eq_rect_r A x F v y H) (F x) v *)
subst.
(* Goal: P (@eq_rect Type A (fun T : Type => T) x A x0) *)
 case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
  P x -> forall y, JMeq x y -> P y.
Proof.
(* Goal: P (@eq_rect Type A (fun T : Type => T) x A x0) *)
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
  P x -> forall y, JMeq x y -> P y.
Proof.
(* Goal: P (@eq_rect Type A (fun T : Type => T) x A x0) *)
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
   P x -> forall y, JMeq y x -> P y.
Proof.
(* Goal: forall (A : Type) (x : A) (P : forall _ : A, Type) (_ : P x) (y : A) (_ : @JMeq A y A x), P y *)
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
   P x -> forall y, JMeq y x -> P y.
Proof.
(* Goal: forall (A : Type) (x : A) (P : forall _ : A, Type) (_ : P x) (y : A) (_ : @JMeq A y A x), P y *)
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
   P x -> forall y, JMeq y x -> P y.
Proof.
(* Goal: forall (A : Type) (x : A) (P : forall _ : A, Type) (_ : P x) (y : A) (_ : @JMeq A y A x), P y *)
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_congr :
 forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
Proof.
(* Goal: forall (A : Type) (x : A) (B : Type) (f : forall _ : A, B) (y : A) (_ : @JMeq A x A y), @eq B (f x) (f y) *)
intros A x B f y H; case JMeq_eq with (1 := H); trivial.
Qed.

(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)

Require Import Coq.Logic.Eqdep.

Lemma JMeq_eq_dep_id :
 forall (A:Type) (B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X:Type => X) A x B y.
Proof.
(* Goal: forall (U : Type) (P : forall _ : U, Type) (p : U) (x : P p) (q : U) (y : P q) (_ : eq_dep U P p x q y), @JMeq (P p) x (P q) y *)
destruct 1.
(* Goal: @JMeq (F y) (@eq_rect_r A x F v y H) (F x) v *)
subst.
(* Goal: @eq A (f A a a') (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) a') *)
rewrite <- eq_rect_eq.
(* Goal: eq_dep Type (fun X : Type => X) B x B x *)
apply eq_dep_intro.
Qed.

Lemma eq_dep_id_JMeq :
 forall (A: Type) (B:Type) (x:A) (y:B), eq_dep Type (fun X:Type => X) A x B y -> JMeq x y.
Proof.
(* Goal: forall (U : Type) (P : forall _ : U, Type) (p : U) (x : P p) (q : U) (y : P q) (_ : eq_dep U P p x q y), @JMeq (P p) x (P q) y *)
destruct 1.
(* Goal: @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) a) *)
apply JMeq_refl.
Qed.

(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *)

Lemma eq_dep_JMeq :
 forall (U: Type) (P: U -> Type) p x q y, eq_dep U P p x q y -> JMeq x y.
Proof.
(* Goal: forall (U : Type) (P : forall _ : U, Type) (p : U) (x : P p) (q : U) (y : P q) (_ : eq_dep U P p x q y), @JMeq (P p) x (P q) y *)
destruct 1.
(* Goal: @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) a) *)
apply JMeq_refl.
Qed.

Lemma eq_dep_strictly_stronger_JMeq :
 exists (U: Type) (P: U -> Type) p q x y, JMeq x y /\ ~ eq_dep U P p x q y.
Proof.
(* Goal: @ex Type (fun U : Type => @ex (forall _ : U, Type) (fun P : forall _ : U, Type => @ex U (fun p : U => @ex U (fun q : U => @ex (P p) (fun x : P p => @ex (P q) (fun y : P q => and (@JMeq (P p) x (P q) y) (not (eq_dep U P p x q y)))))))) *)
exists bool. exists (fun _ => True). exists true. exists false.
(* Goal: @ex True (fun y : True => and (@JMeq True I True y) (not (eq_dep bool (fun _ : bool => True) true I false y))) *)
exists I. exists I.
(* Goal: and (@JMeq True I True I) (not (eq_dep bool (fun _ : bool => True) true I false I)) *)
split.
(* Goal: @JMeq True I True I *)
(* Goal: not (eq_dep bool (fun _ : bool => True) true I false I) *)
trivial.
(* Goal: not (eq_dep bool (fun _ : bool => True) true I false I) *)
intro H.
(* Goal: False *)
assert (true=false) by (destruct H; reflexivity).
(* Goal: False *)
discriminate.
Qed.

(** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
    is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)

Lemma JMeq_eq_dep :
  forall (U:Type) (P:U->Prop) p q (x:P p) (y:P q),
  p = q -> JMeq x y -> eq_dep U P p x q y.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
intros.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
destruct H.
(* Goal: eq_dep U P p x p y *)
apply JMeq_eq in H0 as ->.
(* Goal: @eq (F B) (@eq_rect_r T B F (@eq_rect_r T B F x B (@eq_sym T B B (@eq_refl T B))) B (@eq_refl T B)) x *)
reflexivity.
Qed.

(* Compatibility *)
Notation sym_JMeq := JMeq_sym (only parsing).
Notation trans_JMeq := JMeq_trans (only parsing).

(******************************************

The following is the original floyd/jmeq_lemmas.v

******************************************)

Lemma eq_rect_JMeq: forall (A:Type) (x y: A) (F: A -> Type) (v: F x) (H: x = y), JMeq (eq_rect x F v y H) v.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq (F y) (@eq_rect_r A x F v y H) (F x) v *)
  subst.
(* Goal: @eq A (f A a a') (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) a') *)
  rewrite <- eq_rect_eq.
(* Goal: @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) a) *)
  apply JMeq_refl.
Qed.

Lemma eq_rect_r_JMeq: forall (A:Type) (x y: A) (F: A -> Type) (v: F x) (H: y = x), JMeq (eq_rect_r F v H) v.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq (F y) (@eq_rect_r A x F v y H) (F x) v *)
  subst.
(* Goal: @eq A (f A a a') (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) a') *)
  unfold eq_rect_r; rewrite <- eq_rect_eq.
(* Goal: @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) a) *)
  apply JMeq_refl.
Qed.

Lemma JMeq_sumtype_ll: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: A) (y: C), @eq Type A C -> @eq Type B D -> 
  (@JMeq (A + B) (inl x) (C + D) (inl y)) ->
  JMeq x y.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq B (f x) D (g y) *)
  exists H.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: False *)
  inversion H2.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_sumtype_rr: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: B) (y: D), @eq Type A C -> @eq Type B D -> 
  (@JMeq (A + B) (inr x) (C + D) (inr y)) ->
  JMeq x y.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  exists H0.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: False *)
  inversion H2.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_sumtype_lr: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: A) (y: D), @eq Type A C -> @eq Type B D -> ~ (@JMeq (A + B) (inl x) (C + D) (inr y)).
Proof.
(* Goal: forall (A B C D : Type) (x : B) (y : C) (_ : @eq Type A C) (_ : @eq Type B D), not (@JMeq (sum A B) (@inr A B x) (sum C D) (@inl C D y)) *)
  unfold not.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: False *)
  inversion H2.
Qed.

Lemma JMeq_sumtype_rl: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: B) (y: C), @eq Type A C -> @eq Type B D -> ~ (@JMeq (A + B) (inr x) (C + D) (inl y)).
Proof.
(* Goal: forall (A B C D : Type) (x : B) (y : C) (_ : @eq Type A C) (_ : @eq Type B D), not (@JMeq (sum A B) (@inr A B x) (sum C D) (@inl C D y)) *)
  unfold not.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: False *)
  inversion H2.
Qed.

Ltac solve_JMeq_sumtype H :=
  match type of H with
  | JMeq ?x ?y =>
    destruct x; destruct y;
     [apply JMeq_sumtype_ll in H; auto
     |apply JMeq_sumtype_lr in H; auto; inversion H
     |apply JMeq_sumtype_rl in H; auto; inversion H
     |apply JMeq_sumtype_rr in H; auto]
  end.

Lemma JMeq_inl: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: A) (y: C), @eq Type B D -> JMeq x y -> @JMeq (A + B) (inl x) (C + D) (inl y).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq (sum A B) (@inr A B x) (sum C D) (@inr C D y) *)
  destruct H0 as [?H ?H].
  pose (f_equal2 := 
          fun (A1 : Type) (A2 : Type) (B : Type) (f : forall (_ : A1) (_ : A2), B) 
            (x1 y1 : A1) (x2 y2 : A2) (H : @eq A1 x1 y1) =>
          match H in (eq _ y) return (forall _ : @eq A2 x2 y2, @eq B (f x1 x2) (f y y2)) with
          | eq_refl => fun H0 : @eq A2 x2 y2 => match H0 in (eq _ y) return (@eq B (f x1 x2) (f x1 y)) with
                                                | eq_refl => @eq_refl B (f x1 x2)
                                                end
          end).
(* Goal: @JMeq (sum A B) (@inl A B x) (sum C D) (@inl C D y) *)
  exists (f_equal2 _ _ _ sum _ _ _ _ H0 H).
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: @eq (sum A B) (@eq_rect Type (sum A B) (fun T : Type => T) (@inr A B x) (sum A B) (f_equal2 Type Type Type sum A A B B (@eq_refl Type A) (@eq_refl Type B))) (@inr A B y) *)
  rewrite <- H1.
(* Goal: @eq (prod A C) (@eq_rect Type (prod A C) (fun T : Type => T) (@pair A C a c) (prod A C) (f_equal2 Type Type Type prod A A C C (@eq_refl Type A) (@eq_refl Type C))) (@pair A C (@eq_rect Type A (fun T : Type => T) a A (@eq_refl Type A)) (@eq_rect Type C (fun T : Type => T) c C (@eq_refl Type C))) *)
  unfold f_equal2.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) (f A a a') A (@eq_refl Type A)) (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) (@eq_rect Type A (fun T : Type => T) a' A (@eq_refl Type A))) *)
  simpl.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_inr: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: B) (y: D), @eq Type A C -> JMeq x y -> @JMeq (A + B) (inr x) (C + D) (inr y).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq (sum A B) (@inr A B x) (sum C D) (@inr C D y) *)
  destruct H0 as [?H ?H].
  pose (f_equal2 := 
          fun (A1 : Type) (A2 : Type) (B : Type) (f : forall (_ : A1) (_ : A2), B) 
            (x1 y1 : A1) (x2 y2 : A2) (H : @eq A1 x1 y1) =>
          match H in (eq _ y) return (forall _ : @eq A2 x2 y2, @eq B (f x1 x2) (f y y2)) with
          | eq_refl => fun H0 : @eq A2 x2 y2 => match H0 in (eq _ y) return (@eq B (f x1 x2) (f x1 y)) with
                                                | eq_refl => @eq_refl B (f x1 x2)
                                                end
          end).
(* Goal: @JMeq (sum A B) (@inr A B x) (sum C D) (@inr C D y) *)
  exists (f_equal2 _ _ _ sum _ _ _ _ H H0).
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: @eq (sum A B) (@eq_rect Type (sum A B) (fun T : Type => T) (@inr A B x) (sum A B) (f_equal2 Type Type Type sum A A B B (@eq_refl Type A) (@eq_refl Type B))) (@inr A B y) *)
  rewrite <- H1.
(* Goal: @eq (prod A C) (@eq_rect Type (prod A C) (fun T : Type => T) (@pair A C a c) (prod A C) (f_equal2 Type Type Type prod A A C C (@eq_refl Type A) (@eq_refl Type C))) (@pair A C (@eq_rect Type A (fun T : Type => T) a A (@eq_refl Type A)) (@eq_rect Type C (fun T : Type => T) c C (@eq_refl Type C))) *)
  unfold f_equal2.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) (f A a a') A (@eq_refl Type A)) (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) (@eq_rect Type A (fun T : Type => T) a' A (@eq_refl Type A))) *)
  simpl.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_fst: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: A*B) (y: C*D), @eq Type A C -> @eq Type B D -> JMeq x y -> JMeq (fst x) (fst y).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq B (f x) D (g y) *)
  exists H.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite H2.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_snd: forall (A: Type) (B: Type) (C: Type) (D: Type) (x: A*B) (y: C*D), @eq Type A C -> @eq Type B D -> JMeq x y -> JMeq (snd x) (snd y).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  exists H0.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  destruct H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (@snd A B x) D H0) (@snd C D y) *)
  revert H1 H2.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite <- eq_rect_eq in H2.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (@snd A B x) B (@eq_refl Type B)) (@snd A B y) *)
  rewrite H2.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_pair: forall (A: Type) (B: Type) (C: Type) (D: Type) (a: A) (b: B) (c: C) (d: D), JMeq a b -> JMeq c d -> JMeq (a, c) (b, d).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  destruct H as [?H ?H], H0 as [?H ?H].
  pose (f_equal2 := 
          fun (A1 : Type) (A2 : Type) (B : Type) (f : forall (_ : A1) (_ : A2), B) 
            (x1 y1 : A1) (x2 y2 : A2) (H : @eq A1 x1 y1) =>
          match H in (eq _ y) return (forall _ : @eq A2 x2 y2, @eq B (f x1 x2) (f y y2)) with
          | eq_refl => fun H0 : @eq A2 x2 y2 => match H0 in (eq _ y) return (@eq B (f x1 x2) (f x1 y)) with
                                                | eq_refl => @eq_refl B (f x1 x2)
                                                end
          end).
(* Goal: @JMeq (prod A C) (@pair A C a c) (prod B D) (@pair B D b d) *)
  exists (f_equal2 _ _ _ prod _ _ _ _ H H0).
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: @eq B (@eq_rect Type A (fun T : Type => T) (f A a a') B H0) (f B b b') *)
  rewrite <- H1, <- H2.
(* Goal: @eq (prod A C) (@eq_rect Type (prod A C) (fun T : Type => T) (@pair A C a c) (prod A C) (f_equal2 Type Type Type prod A A C C (@eq_refl Type A) (@eq_refl Type C))) (@pair A C (@eq_rect Type A (fun T : Type => T) a A (@eq_refl Type A)) (@eq_rect Type C (fun T : Type => T) c C (@eq_refl Type C))) *)
  unfold f_equal2.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) (f A a a') A (@eq_refl Type A)) (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) (@eq_rect Type A (fun T : Type => T) a' A (@eq_refl Type A))) *)
  simpl.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma eq_rect_r_eq_rect_r_eq_sym: forall {T} {A B: T} F x (H: A = B),
  eq_rect_r F (eq_rect_r F x H) (eq_sym H) = x.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @eq (F B) (@eq_rect_r T B F (@eq_rect_r T B F x B (@eq_sym T B B (@eq_refl T B))) B (@eq_refl T B)) x *)
  reflexivity.
Qed.

Lemma eq_rect_r_eq_rect_r_eq_sym': forall {T} {A B: T} F x (H: B = A),
  eq_rect_r F (eq_rect_r F x (eq_sym H)) H = x.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @eq (F B) (@eq_rect_r T B F (@eq_rect_r T B F x B (@eq_sym T B B (@eq_refl T B))) B (@eq_refl T B)) x *)
  reflexivity.
Qed.

Lemma JMeq_func: forall (A: Type) (B: Type) (C: Type) (D: Type) (f: A -> B) (g: C -> D) x y,
  @eq Type B D ->
  JMeq x y -> JMeq f g -> JMeq (f x) (g y).
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq B (f x) D (g y) *)
  exists H.
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H0 as [?H ?H], H1 as [?H ?H].
(* Goal: @eq D (@eq_rect Type B (fun T : Type => T) (f x) D H) (g y) *)
  destruct H, H0.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (f x) B (@eq_refl Type B)) (g y) *)
  rewrite <- eq_rect_eq in H3.
(* Goal: @eq B (@eq_rect Type B (fun T : Type => T) (f x) B (@eq_refl Type B)) (g y) *)
  rewrite H3, <- H2.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma eq_JMeq: forall A (x y: A), x=y -> JMeq x y.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
Proof. intros. subst. apply JMeq_refl.
Qed.

Lemma list_func_JMeq: forall {A: Type} {B: Type} {C: Type} (a: list A) (b: list B) (f: forall X, list X -> C), @eq Type A B -> JMeq a b -> f A a = f B b.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @eq C (f A a) (f B b) *)
  destruct H0 as [? ?].
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @eq C (f A a) (f A b) *)
  rewrite <- eq_rect_eq in e.
(* Goal: @eq C (f A a) (f A b) *)
  rewrite e.
(* Goal: @eq C (f A b) (f A b) *)
  auto.
Qed.

Lemma list_func_JMeq': forall {A: Type} {B: Type} (a: list A) (b: list B) (a': A) (b': B) (f: forall X, list X -> X -> X), JMeq a b -> JMeq a' b' -> JMeq (f A a a') (f B b b').
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  destruct H as [?H ?H], H0 as [?H ?H].
(* Goal: @JMeq A (f A a a') B (f B b b') *)
  exists H0.
(* Goal: @eq B (@eq_rect Type A (fun T : Type => T) (f A a a') B H0) (f B b b') *)
  rewrite <- H1, <- H2.
(* Goal: @eq B (@eq_rect Type A (fun T : Type => T) (f A a a') B H0) (f B (@eq_rect Type (list A) (fun T : Type => T) a (list B) H) (@eq_rect Type A (fun T : Type => T) a' B H0)) *)
  destruct H0.
(* Goal: @eq A (@eq_rect Type A (fun T : Type => T) (f A a a') A (@eq_refl Type A)) (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) (@eq_rect Type A (fun T : Type => T) a' A (@eq_refl Type A))) *)
  simpl.
(* Goal: @eq A (f A a a') (f A (@eq_rect Type (list A) (fun T : Type => T) a (list A) H) a') *)
  rewrite <- eq_rect_eq.
(* Goal: @eq A (f A a a') (f A a a') *)
  apply eq_refl.
Qed.

Lemma JMeq_sigT: forall {A: Type} {B: Type} (a: A), @eq Type A B -> {b: B | JMeq a b}.
Proof.
(* Goal: forall (A B : Type) (a : A) (_ : @eq Type A B), @sig B (fun b : B => @JMeq A a B b) *)
  intros.
(* Goal: @sig B (fun b : B => @JMeq A a B b) *)
  unfold JMeq.
(* Goal: @sig B (fun b : B => @sig (@eq Type A B) (fun H : @eq Type A B => @eq B (@eq_rect Type A (fun T : Type => T) a B H) b)) *)
  destruct H.
(* Goal: @sig A (fun b : A => @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) b)) *)
  exists a.
(* Goal: @sig (@eq Type A A) (fun H : @eq Type A A => @eq A (@eq_rect Type A (fun T : Type => T) a A H) a) *)
  apply JMeq_refl.
Qed.

Arguments JMeq_eq {A} {x y} _.
