fact: Definition append s1 s2 := match s1,s2 with | Leaf _, _ => s2 | _, Leaf _ => s1 | _, Node h2 l2 x2 d2 r2 => let '(s2',(x,d)) := remove_min l2 x2 d2 r2 in bal s1 x d s2' end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)