proposition: Lemma SCC_incl : R1 << R2 -> SCC R1 << SCC R2.
proof: Proof. intros. unfold inclusion; unfold SCC. intros. destruct H0. assert (R1! << R2!). apply tc_incl; hyp. split; unfold inclusion in H2. apply (H2 x y); hyp. apply (H2 y x); hyp. Qed.
imports: CoLoR(Cycle Path ListUtil RelUtil LogicUtil)