A,B,C:V List. A-- > *C 
B-- > *C 
A @ B-- > *Cx:T, l1,l2:T List. (x 
l1 @ l2) 
(x l1) (x l2)| Rank | Theorem | Name |
| 3 | Thm* For any graph
A,B,C:V List. A-- > *C B-- > *C A @ B-- > *C | [list-list-connect-append2] |
| cites | ||
| 2 | Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) | [member_append] |