fact: Definition inter (t1 t2: t) : t := match compare_height t1 t1 t2 t2 with | Lt => filter (fun k => mem k t2) t1 | Gt => filter (fun k => mem k t1) t2 | Eq => linear_inter t1 t2 end.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat