fact: Definition merge (m1 : t elt) (m2 : t elt') : t elt'' := treeify (mergeL (rev_bindings m1) (rev_bindings m2) nil).
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)