i,j:V. [i]-- > *j 
i-the_graph- > *jP:(T
Prop). (
x
nil.P(x)) FalseP:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) 
(yL.P(y))| Rank | Theorem | Name |
| 3 | Thm* For any graph
i,j:V. [i]-- > *j i-the_graph- > *j | [list-connect-singleton] |
| cites | ||
| 1 | Thm* P:(TProp). (xnil.P(x)) False | [l_exists_nil] |
| 2 | Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y)) | [l_exists_cons] |