misc.JMrelation

Require Import Relation_Definitions RelationClasses.
Require Export Unicode.Utf8 Utf8_core.

Inductive R {A: Type} (r: relation A) (x: A): forall B: Type, relation B B Prop := relate y: r x y R r x A r y.

Lemma reflexive A (x:A) (Ra: relation A) `{!Reflexive Ra}: R Ra x _ Ra x.

Lemma symmetric A B (x:A) (Ra: relation A) (Rb: relation B) (y:B) `{!Symmetric Ra}: R Ra x _ Rb y R Rb y _ Ra x.

Lemma transitive A B C (Ra: relation A) (Rb: relation B) (Rc: relation C) (a:A) (b:B) (c:C) `{!Transitive Ra}:
  R Ra a _ Rb b R Rb b _ Rc c R Ra a _ Rc c.

Require Import Eqdep.

Lemma unJM A (r: relation A) (x y:A) r' (E: R r x A r' y): r x y.