fact: Fixpoint xfoldi (m : t A) (v : B) (i : key) := match m with | Leaf _ => v | Node l (Some x) r => xfoldi r (f i x (xfoldi l v (append i 2))) (append i 3) | Node l None r => xfoldi r (xfoldi l v (append i 2)) (append i 3) end.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface