proposition: Lemma mem_succs_id : forall g x y, XSet.mem y (succs x g) = true -> g U id x y == g.
proof: Proof. intros g x y h. split. rewrite union_incl_eq. split. refl. intros a b [xa yb]. rewrite xa, yb. rewrite <- mem_succs_rel. hyp. apply incl_union_l. refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)