proposition: Lemma In_succs_rel : forall g x y, XSet.In y (succs x g) <-> rel g x y.
proof: Proof. intros. unfold succs, rel. destruct (find x g) as [t|]; split_all. ex t. tauto. inversion H. hyp. revert H. set_iff. tauto. discr. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)