proposition: Lemma succ_list_cons : forall x y l, succ_list x (y :: l) == id x y U succ_list x l.
proof: Proof. intros x y l. apply rel_eq; intros a b. unfold Relation_Operators.union, succ_list, id. rewrite InA_cons. fo. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)