proposition: Fact append_bb_match ll lx lv lr rl rx rv rr : rspec (fun a x e b => Rd (Bk ll lx lv a) x e (Bk b rx rv rr)) (fun t => lbalS ll lx lv (Bk t rx rv rr)) (append lr rl) (append (Bk ll lx lv lr) (Bk rl rx rv rr)).
proof: Proof. exact (rmatch _ _ _). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)