L:T List, x,y:T. x before y 
L 
(
L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3))l:T List, a,x,y:T. x before y [a / l] x = a & (y l) 
x before y ls:T List, z:T. (z s) 
(s1,s2:T List. s = (s1 @ [z / s2]))| Rank | Theorem | Name |
| 3 | Thm* L:T List, x,y:T. x before y L (L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3)) | [l_before-iff] |
| cites | ||
| 2 | Thm* l:T List, a,x,y:T. x before y [a / l] x = a & (y l) x before y l | [cons_before] |
| 2 | Thm* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2])) | [l_member_decomp] |