proposition: Fact append_rr_match ll lx lv lr rl rx rv rr : rspec (fun a x e b => Rd (Rd ll lx lv a) x e (Rd b rx rv rr)) (fun t => Rd ll lx lv (Rd t rx rv rr)) (append lr rl) (append (Rd ll lx lv lr) (Rd 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)