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