fact: Fixpoint sublist T (l r : T -> bool) (u:order T) {struct u} : list T := match u with ostop t => if (l t) then if (r t) then (cons t (nil T)) else (nil T) else (nil T) | onode a v w => match (l (rightmost v)), (r (leftmost w)) with true, true => concatenate (sublist l r v) (sublist l r w) | false, true => sublist l r w | true, false => sublist l r v | false, false => nil T end end.