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 p l inlist. destruct p. absurd (InA eqke (t0, e) ((t0, e) :: l));auto. Qed.
imports: FMapInterface