proposition: Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
proof: Proof. induction m as [|[a m]]; intros x e H; simpl in *; [congruence|]. destruct X.compare; [congruence| |]. - apply InA_cons_hd; split; compute; congruence. - apply InA_cons_tl; apply IHm; auto. Qed.
imports: FMapInterface