proposition: Lemma eq_dep_strictly_stronger_JMeq : exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y.
proof: Proof. exists bool. exists (fun _ => True). exists true. exists false. exists I. exists I. split. - trivial. - intro H. assert (true=false) by (destruct H; reflexivity). discriminate. Qed.
imports: Eqdep Eqdep