proposition: Fact lbalS_match l x vx r : rspec (fun a y vy b => Rd (Bk a y vy b) x vx r) (fun l => match r with | Bk a y vy b => rbal' l x vx (Rd a y vy b) | Rd (Bk a y vy b) z vz c => Rd (Bk l x vx a) y vy (rbal' b z vz (makeRed c)) | _ => Rd l x vx r end) l (lbalS l x vx r).
proof: Proof. exact (rmatch _ _ _). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)