proposition: Lemma rel_add_edge : forall x y g, add_edge x y g == g U id x y.
proof: Proof. intros. rewrite rel_eq; intros a b. unfold add_edge, Relation_Operators.union, id. split_all. destruct H as [sa [a1 a2]]. rewrite add_o in a1. destruct (eq_dec x a). inversion a1. subst sa. rewrite add_iff in a2. rewrite In_succs_rel in a2. rewrite e in a2. split_all. auto with ordered_type. left. exists sa. tauto. destruct H as [sa [a1 a2]]. unfold rel. rewrite add_o. destruct (eq_dec x a). exists (XSet.add y (succs x g)). split_all. rewrite add_iff. right. rewrite e, In_succs_rel. exists sa. auto. exists sa. auto. unfold rel. rewrite add_o. destruct (eq_dec x a). exists (XSet.add y (succs x g)). split_all. rewrite add_iff. auto with ordered_type. absurd (eq x a); hyp. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)