proposition: Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
proof: Proof. intros m x; functional induction (find x m); subst; intros; clearf; try discriminate. - constructor 2; auto. - inversion H; auto. - constructor 3; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int