proposition: Lemma In_preds_rel : forall x y g, XSet.In x (preds y g) <-> rel g x y.
proof: Proof. intros x y g. pattern g; apply map_induction_bis; clear g. intros m m' mm' h. rewrite <- mm'. hyp. rewrite preds_empty. split. intro h. revert h. set_iff. tauto. intros [s [s1 s2]]. rewrite empty_o in s1. discr. intros z s g n h. rewrite preds_add. 2: hyp. case_eq (XSet.mem y s); intros. rewrite add_iff. rewrite h. split. intros [h'|h']. exists s. rewrite add_eq_o. rewrite mem_iff. intuition. hyp. destruct h' as [t [t1 t2]]. exists t. rewrite add_o. destruct (eq_dec z x). rewrite not_find_in_iff, e in n. rewrite n in t1. discr. tauto. intros [t [t1 t2]]. rewrite add_o in t1. destruct (eq_dec z x). auto. right. exists t. tauto. rewrite h. split. intros [t [t1 t2]]. exists t. rewrite add_o. destruct (eq_dec z x). rewrite not_find_in_iff, e in n. rewrite n in t1. discr. tauto. intros [t [t1 t2]]. rewrite add_o in t1. destruct (eq_dec z x). inversion t1. subst t. rewrite XSetFacts.mem_iff in t2. rewrite H in t2. discr. exists t. tauto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)