proposition: Lemma lift_transitivity_left (y x z : X): E x y -> R y z -> R x z.
proof: Proof. destruct H as [Hequiv Hproper]; intros G;rewrite G. trivial. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)