proposition: Lemma is_empty_1 :forall m, Empty m -> is_empty m = true.
proof: Proof. unfold Empty, PX.MapsTo. intros m. case m;auto. intros (k,e) l inlist. absurd (InA eqke (k, e) ((k, e) :: l)); auto with ordered_type. Qed.
imports: FMapInterface