proposition: Lemma mem_succs_rel : forall g x y, XSet.mem y (succs x g) = true <-> rel g x y.
proof: Proof. intros. rewrite <- mem_iff. apply In_succs_rel. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)