proposition: Lemma succ_list_nil : forall x, succ_list x nil == empty_rel.
proof: Proof. intro x. rewrite rel_eq; intros a b. unfold succ_list, empty_rel. split_all. inversion H0. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)