proposition: Fact lbal_match l k v r : rrspec (fun a x vx b y vy c => Rd (Bk a x vx b) y vy (Bk c k v r)) (fun l => Bk l k v r) l (lbal 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)