proposition: Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
proof: Proof. intros. unfold Empty. split; intros. - assert (forall a, ~ List.In a (elements m)). { red; intros. apply (H (fst a) (snd a)). rewrite elements_mapsto_iff. rewrite InA_alt; exists a; auto. split; auto; split; auto. } destruct (elements m); auto. elim (H0 p); simpl; auto. - red; intros. rewrite elements_mapsto_iff in H0. rewrite InA_alt in H0; destruct H0. rewrite H in H0; destruct H0 as (_,H0); inversion H0. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface