fact: Definition makeRed m : t := match m with | Leaf => Leaf | Node _ a x v b => Rd a x v b end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)