fact: Fixpoint mapoL (l : klist elt)(acc : klist elt') : klist elt' := match l with | nil => acc | (k,v)::l => mapoL l (ocons k (f k v) acc) end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)