l:T List, a,x,y:T.
Thm* x before y
[a / l] 
x = a & (y l) 
x before y lx1,x2:T, L1,L2:T List.
Thm* [x1 / L1]
[x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2x:T, L:T List. (x L) [x] L| Rank | Theorem | Name |
| 2 | l:T List, a,x,y:T.
Thm* x before y [a / l] x = a & (y l) x before y l | [cons_before] |
| cites the following: | ||
| 1 | x1,x2:T, L1,L2:T List.
Thm* [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 | [cons_sublist_cons] |
| 0 | x:T, L:T List. (x L) [x] L | [member_iff_sublist] |