fact: Fixpoint diff s1 s2 := match s1, s2 with | Leaf, _ => Leaf | _, Leaf => s1 | Node _ l1 x1 r1, _ => let (l2',pres,r2') := split x1 s2 in if pres then concat (diff l1 l2') (diff r1 r2') else join (diff l1 l2') x1 (diff r1 r2') end.
imports: FunInd MSetInterface MSetGenTree BinInt Int