fact: Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) := match m with | Leaf => acc | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l end.
imports: FunInd FMapInterface FMapList ZArith Int