proposition: Lemma JMeq_eq_dep : forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y.
proof: Proof. intros U P p q x y H H0. destruct H. apply JMeq_eq in H0 as ->. reflexivity. Qed.
imports: Eqdep Eqdep