proposition: Lemma unJM A (r: relation A) (x y:A) r' (E: R r x A r' y): r x y.
proof: Proof. simple inversion E. rewrite (eq_rect_eq__eq_dep_eq _ (eq_rect_eq _) _ _ _ _ (eq_sigT_eq_dep _ _ _ _ _ _ H2)). firstorder. Qed.
imports: Relation_Definitions Setoid Unicode.Utf8 Utf8_core Coq.Logic.Eqdep