proposition: Lemma union_list_spec : forall (A : Type) L (x y : A) (r : relation A), In r L -> r x y -> fold_right (@union A) empty L x y.
proof: Proof. intros. induction L. simpl in *; tauto. simpl in *. destruct H. destruct H. subst; left; auto. right; tauto. Qed.
imports: Coq(Permutation Multiset Setoid PermutSetoid) CoLoR(SCCTopoOrdering AGraph ATrs RelUtil RelSub BoundNat AdjMat LogicUtil NatUtil SCC SCC_dec ListExtras SN VecUtil GDomainBij OptUtil Union SortUtil ListNodup ListPermutation)