A:V List, x:V. A-- > *[x] 
A-- > *xP:(T
Prop). (x
nil.P(x))P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))| Rank | Theorem | Name |
| 3 | Thm* For any graph
A:V List, x:V. A-- > *[x] A-- > *x | [list-list-connect-singleton] |
| cites | ||
| 0 | Thm* P:(TProp). (xnil.P(x)) | [l_all_nil] |
| 2 | Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) | [l_all_cons] |