proposition: Lemma rel_map_fold_add_pred_ext : forall x s g g0 a b, rel (fold (add_pred x s) g g0) a b <-> pred x s g a b \/ rel g0 a b.
proof: Proof. split; intro h. apply rel_map_fold_add_pred in h. hyp. apply rel_map_fold_add_pred. hyp. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)