proposition: Lemma In_Union_elim : forall cs x y, Union cs x y -> exists ci, In ci cs /\ hd_red_Mod S ci x y.
proof: Proof. induction cs; simpl; intros. contr. destruct H. exists a. intuition. destruct (IHcs _ _ H). exists x0. intuition. Qed.
imports: CoLoR(AGraph Union ATrs RelUtil ListUtil LogicUtil SN BoolUtil VecUtil)