proposition: Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
proof: Proof. intros m x. unfold PX.MapsTo. induction m; simpl;intros e' eqfind; inversion eqfind; auto. destruct a, X.eq_dec. + constructor; split; simpl; congruence. + constructor 2; apply IHm; assumption. Qed.
imports: FMapInterface