proposition: Lemma rel_empty : rel empty == empty_rel.
proof: Proof. rewrite rel_eq; intros a b. unfold empty_rel. split_all. destruct H as [sa [a1 a2]]. rewrite <- find_mapsto_iff in a1. rewrite empty_mapsto_iff in a1. hyp. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)