proposition: Lemma union_list_spec2 : forall (A : Type) L (x y : A), fold_right (@union A) empty L x y -> exists r, In r L /\ r x y.
proof: Proof. intros. induction L. simpl in *; tauto. simpl in *. destruct H. exists a; split; tauto. destruct (IHL H). exists x0. split; try 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)