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