proposition: Lemma trans_clos_right : forall R' x y, trans_clos R x y -> trans_clos (union _ R' R) x y.
proof: Proof. intros R' x y H. induction H. constructor. right; assumption. constructor 2 with y. right;assumption. assumption. Qed.
imports: CoLoR(closure) Coq(Relation_Operators)