fact: Fixpoint append (l:t) : t -> t := match l with | Leaf => fun r => r | Node lc ll lx lv lr => fix append_l (r:t) : t := match r with | Leaf => l | Node rc rl rx rv rr => match lc, rc with | Red, Red => let lrl := append lr rl in match lrl with | Rd lr' x v rl' => Rd (Rd ll lx lv lr') x v (Rd rl' rx rv rr) | _ => Rd ll lx lv (Rd lrl rx rv rr) end | Black, Black => let lrl := append lr rl in match lrl with | Rd lr' x v rl' => Rd (Bk ll lx lv lr') x v (Bk rl' rx rv rr) | _ => lbalS ll lx lv (Bk lrl rx rv rr) end | Black, Red => Rd (append_l rl) rx rv rr | Red, Black => Rd ll lx lv (append lr r) end end end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)