proposition: Lemma lift_transitivity_right (y x z : X): E y z -> R x y -> 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)