proposition: Fact lbalS_match l x r : rspec (fun a y b => Rd (Bk a y b) x r) (fun l => match r with | Bk a y b => rbal' l x (Rd a y b) | Rd (Bk a y b) z c => Rd (Bk l x a) y (rbal' b z (makeRed c)) | _ => Rd l x r end) l (lbalS l x r).
proof: Proof. exact (rmatch _ _ _). Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat