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