Set Implicit Arguments.
Unset Strict Implicit.

Axiom proof_irrelevance : forall (P:Prop) (p q:P), p = q.

Inductive JMeq (A:Type) (a:A) : forall (B:Type) (b:B), Prop :=
    JMeq_refl : JMeq a a
 
 .

Infix "-=-" := JMeq (left associativity, at level 90).

Definition transport : forall (A B:Type) (AeqB:A = B) (a:A), B.
Proof.
destruct 1; intro a; exact a.
Defined.

Section JMeq_transport_eqT.
  Variables (A B : Type) (a : A) (b : B) (H : a -=- b) (HT : A = B).

  Local P (X:Type) (x:X) : Prop := forall E:X = B, transport E x = b.

  Remark Pb : P b.
  Proof.
  unfold P; intros.
  cut (refl_equal B = E).
  destruct 1; split.
  apply proof_irrelevance.
  Qed.

  Remark Pa : P a.
  Proof.
  cut (P b).
  cut (b -=- a).
  destruct 1; tauto.
  elim H; split.
  exact Pb.
  Qed.

  Lemma JMeq_transport_eqT : transport HT a = b.
  Proof.
  cut (P a).
  unfold P; intros.
  apply (H0 HT).
  exact Pa.
  Qed.
End JMeq_transport_eqT.

Theorem JMeq_eqT : forall (A:Type) (a b:A), (a -=- b) -> a = b.
Proof.
intros.
transitivity (transport (refl_equal A) a).
split.
apply JMeq_transport_eqT.
assumption.
Qed.

Theorem JMeq_eq : forall (A:Set) (a b:A), (a -=- b) -> a = b.
Proof.
intros; cut (a = b). 
destruct 1; split.
apply JMeq_eqT; assumption.
Qed.