fact: Definition obind {A B} (o:option A) (f:A->option B) := match o with Some a => f a | None => None end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)