proposition: Lemma succ_empty : forall x, succ x XSet.empty == empty_rel.
proof: Proof. intro x. rewrite rel_eq; intros a b. unfold succ, empty_rel. split_all. revert H0. set_iff. auto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)