L:T List, a,b:T. a before b 
L 
(a L)x:T, L:T List. (x L) 
[x] 
LL1,L2,L3:T List. L1 L2 L2 L3 L1 L3x1,x2:T, L1,L2:T List.
Thm* [x1 / L1]
[x2 / L2] x1 = x2 & L1 L2 
[x1 / L1] L2L:T List. nil L True| Rank | Theorem | Name |
| 3 | L:T List, a,b:T. a before b L (a L) | [l_before_member2] |
| cites the following: | ||
| 0 | x:T, L:T List. (x L) [x] L | [member_iff_sublist] |
| 2 | L1,L2,L3:T List. L1 L2 L2 L3 L1 L3 | [sublist_transitivity] |
| 1 | x1,x2:T, L1,L2:T List.
Thm* [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 | [cons_sublist_cons] |
| 0 | L:T List. nil L True | [nil_sublist] |