A,B:V List. B 
A 
A-- > *Bl1,l2:T List, x:T. l1 l2 (x 
l1) (x l2)| Rank | Theorem | Name |
| 3 | Thm* For any graph
A,B:V List. B A A-- > *B | [list-list-connect-iseg] |
| cites | ||
| 2 | Thm* l1,l2:T List, x:T. l1 l2 (x l1) (x l2) | [iseg_member] |