proposition: Lemma trans_clos_left : 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. left; assumption. constructor 2 with y. left;assumption. assumption. Qed.
imports: CoLoR(closure) Coq(Relation_Operators)