proposition: Lemma xgmapi: forall (A B: Type) (f: key -> A -> B) (i j : key) (m: t A), find i (xmapi f m j) = option_map (f (append j i)) (find i m).
proof: Proof. induction i; intros; destruct m; simpl; auto. - rewrite (append_assoc_1 j i); apply IHi. - rewrite (append_assoc_0 j i); apply IHi. - rewrite (append_neutral_r j); auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface