proposition: Fact rbal'_match l k v r : rrspec (fun a x vx b y vy c => Rd (Bk l k v a) x vx (Bk b y vy c)) (fun r => Bk l k v r) r (rbal' l k v r).
proof: Proof. exact (rrmatch' _ _ _). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)