Rank | Theorem | Name |
3 | Thm* L:T List, a,b:T. a before b L  (b L) | [l_before_member] |
cites the following: |
0 | Thm* x:T, L:T List. (x L)  [x] L | [member_iff_sublist] |
2 | Thm* L1,L2,L3:T List. L1 L2  L2 L3  L1 L3 | [sublist_transitivity] |
2 | Thm* L1,L2:T List. null(L2)  L1 tl(L2)  L1 L2 | [sublist_tl] |
1 | Thm* L1,L2:T List. L1 = L2  L1 L2 | [sublist_weakening] |