fact: Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) : t elt' := match m with | Leaf _ => Leaf _ | Node l x d r h => match f x d with | Some d' => join (map_option f l) x d' (map_option f r) | None => concat (map_option f l) (map_option f r) end end.
imports: FunInd FMapInterface FMapList ZArith Int