proposition: Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
proof: Proof. induction m; simpl; inversion_clear 1; auto. - exists k; auto with ordered_type. - destruct (IHm1 _ _ H0). exists x0; intuition. - destruct (IHm2 _ _ H0). exists x0; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int