fact: Definition oelse {A} (o1 o2:option A) := match o1 with | Some x => Some x | None => o2 end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)