proposition: Lemma preds_geq_empty : forall x g, geq g empty -> preds x g [=] XSet.empty.
proof: Proof. intros x g. pattern g; apply map_induction_bis; clear g. intros m m' mm' h hm'. rewrite <- mm'. apply h. rewrite mm'. hyp. intros _. unfold preds. rewrite fold_empty. refl. intros y s g n h e. rewrite preds_add. 2: hyp. case_eq (XSet.mem x s); intros. ded (geq_add n e). rewrite (mem_is_empty H) in H0. ded (H0 y). rewrite empty_o, succs_empty, add_o in H1. destruct (eq_dec y y). discr. absurd (eq y y). hyp. refl. apply h. ded (geq_add_remove n e). rewrite H0. destruct (XSet.is_empty s). refl. rewrite remove_empty. refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)