proposition: Lemma find_Some_rel {g x s} : find x g = Some s -> XSet.is_empty s = false -> exists y, rel g x y.
proof: Proof. intros hx hs. destruct (choose_mem_3 _ hs) as [y [h1 h2]]. rewrite <- mem_iff in h2. ex y s. tauto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)