fact: Fixpoint triage (l:list term)(f:term -> bool) (r : mopair) {struct l}: mopair:= match l with nil => r | cons a m => let c := triage m f r in if (fits_impl_pattern a) then mop (cons a (imp_list c)) (stat_ord c) else if (f a) then c else mop (imp_list c) (insert term_ineqL a (stat_ord c)) end.