proposition: Theorem gmapi: forall (A B: Type) (f: key -> A -> B) (i: key) (m: t A), find i (mapi f m) = option_map (f i) (find i m).
proof: Proof. intros. unfold mapi. replace (f i) with (f (append xH i)). - apply xgmapi. - rewrite append_neutral_l; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface