fact: Fixpoint gmerge m1 m2 := match m1, m2 with | Leaf _, _ => mapr m2 | _, Leaf _ => mapl m1 | Node h1 l1 x1 d1 r1, _ => let (l2',o2,r2') := split x1 m2 in match f x1 d1 o2 with | Some e => join (gmerge l1 l2') x1 e (gmerge r1 r2') | None => concat (gmerge l1 l2') (gmerge r1 r2') end end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)