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