proposition: Lemma rel_map_fold_add_pred : forall x s g g0, fold (add_pred x s) g g0 == pred x s g U g0.
proof: Proof. intros x s g g0. pattern g, (fold (add_pred x s) g g0). apply fold_rec_weak; clear g. intros m n g mn h. apply Equal_geq in mn. rewrite h. apply union_same. apply pred_geq; (refl||hyp). refl. rewrite pred_empty, R.union_empty_l. refl. intros z t g m n h. unfold add_pred. case_eq (XSet.mem x t); intros. rewrite <- mem_iff in H. rewrite rel_set_fold_add_edge, h, <- R.union_assoc. apply R.union_same. 2: refl. rewrite rel_eq; intros a b. unfold succ, pred, Relation_Operators.union. split_all. rewrite H0. unfold rel. exists t. rewrite add_eq_o. tauto. refl. unfold rel. rewrite add_o. destruct (eq_dec z a). exists t. tauto. destruct H0 as [u [u1 u2]]. exists u. tauto. unfold rel in H0. rewrite add_o in H0. destruct (eq_dec z a). left. rewrite (eq_com a z). tauto. right. tauto. rewrite <- not_mem_iff in H. rewrite h. apply R.union_same. 2: refl. rewrite rel_eq; intros a b. unfold pred. rewrite not_find_in_iff in n. split_all. unfold rel. rewrite add_o. destruct (eq_dec z a). 2: hyp. rewrite e in n. destruct H0 as [u [u1 u2]]. rewrite n in u1. discr. unfold rel in H0. rewrite add_o in H0. destruct (eq_dec z a). 2: hyp. destruct H0 as [u [u1 u2]]. inversion u1. subst t. contr. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)