proposition: Lemma pred_empty : forall x s, pred x s empty == empty_rel.
proof: Proof. split; intros a b; unfold pred, empty_rel; intros. destruct H. destruct H as [t [t1 t2]]. rewrite empty_o in t1. discr. contr. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)