proposition: Lemma gle_succs : forall g g', gle g g' <-> forall x, succs x g [<=] succs x g'.
proof: Proof. intros g g'. split. intros gg' x. rewrite gg'. refl. intro h. intros x y. rewrite <- !In_succs_rel. rewrite (h x). auto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)