fact: Fixpoint xelements (m : t A) (i : key) : list (key * A) := match m with | Leaf => nil | Node l None r => (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH))) | Node l (Some x) r => (xelements l (append i (xO xH))) ++ ((i, x) :: xelements r (append i (xI xH))) end.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface