proposition: Lemma Equiv_empty : forall m, Equiv eq empty m <-> Empty m.
proof: Proof. intro m. unfold Equiv, Empty. intuition. assert (In a m). exists e. hyp. rewrite <- H0 in H2. rewrite empty_in_iff in H2. hyp. rewrite empty_in_iff in H0. contr. rewrite empty_in_iff. destruct H0. eapply H. apply H0. assert (In k (@empty A)). exists e. hyp. rewrite empty_in_iff in H2. contr. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)