| Rank | Theorem | Name |
| 2 | Thm* For any graph
 x,y,z:V. x-the_graph- > *y   y-the_graph- > *z x-the_graph- > *z | [connect_transitivity] |
| cites |
| 1 | Thm* as,bs:T List, i: ||as||. (as @ bs)[i] = as[i] | [select_append_front] |
| 0 | Thm* a:T, as:T List, i: . 0 < i i ||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |
| 1 | Thm* as,bs:T List, i:{||as||..(||as||+||bs||) }. (as @ bs)[i] = bs[(i-||as||)] | [select_append_back] |
| 0 | Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||  | [length_append] |
| 1 | Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] | [select_tl] |
| 0 | Thm* l:A List. ||l|| 1 ||tl(l)|| = ||l||-1 | [length_tl] |
| 0 | Thm* l:T List. (l @ nil) ~ l | [append_nil_sq] |