fact: Fixpoint xmapi (m : t A) (i : key) : t B := match m with | Leaf => @Leaf B | Node l o r => Node (xmapi l (append i (xO xH))) (option_map (f i) o) (xmapi r (append i (xI xH))) end.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface