fact: Fixpoint compare_cont s1 (cont:enumeration -> comparison) e2 := match s1 with | Leaf => cont e2 | Node _ l1 x1 d1 r1 => compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2 end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)