proposition: Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
proof: Proof. destruct m as [|(x,e) m]; simpl; intuition; try discriminate. specialize (H x). revert H. now dec. Qed.
imports: Coq(EqualitiesFacts)