proposition: Lemma preds_add : forall x y s g, ~In y g -> preds x (add y s g) [=] if XSet.mem x s then XSet.add y (preds x g) else preds x g.
proof: Proof. intros x y s g nyg. unfold preds. rewrite fold_add. refl. fo. apply preds_aux_m'. refl. apply preds_aux_transp. hyp. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)