fact: Definition rcase {A} f g m : A := match m with | Rd a x v b => f a x v b | _ => g m end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)