proposition: Lemma JMeq_same_inv : forall (A : Type) (x y : A), JMeq x y -> x = y.
proof: Proof. Proof using. introv E. apply (@eq_dep_same_inv Type (fun T => T)). apply~ eq_dep_of_JMeq. Qed.
imports: TLC(LibTactics LibAxioms) Coq.Logic.JMeq