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