Lines Matching refs:same
193 <=> t <= q by sublist_def, same heads
245 <=> (t <= q) and (q <= t) by sublist_def, same heads
333 Then t <= q by sublist_def, same heads
527 If h' = h, t <= y by sublist_def, same heads
588 By induction on list p, and note that p and (p ++ q) have the same head.
648 Then t ++ h::q <= q by sublist_def, same heads
726 Then t ++ [h'] <= q ++ [h'] by sublist_def, same heads
795 For this case, choose x=[], y=q, and sublist (h::t) (h::q) = sublist t q, by SUBLIST same head.
801 hence sublist t y = sublist t q ==> sublist (h::t) (h::q) by SUBLIST same head.
859 Then t <= q by sublist_def, same heads
892 Then t <= q by sublist_def, same heads