fact: Fixpoint join l : elt -> t -> t := match l with | Leaf => add | Node lh ll lx lr => fun x => fix join_aux (r:t) : t := match r with | Leaf => add x l | Node rh rl rx rr => if (rh+2) <? lh then bal ll lx (join lr x r) else if (lh+2) <? rh then bal (join_aux rl) rx rr else create l x r end end.
imports: FunInd MSetInterface MSetGenTree BinInt Int