is mentioned by

Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfsl-traversal(the_graph;L1;s) dfsl-traversal(the_graph;L1 @ L2;s)	[dfsl-traversal-append]
Thm* For any graph L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s)	[dfl-traversal-connect]
Thm* For any graph A,B,C:V List. A-- > *C B-- > *C A @ B-- > *C	[list-list-connect-append2]
Thm* For any graph A,B,C:V List. A-- > *B @ C A-- > *B & A-- > *C	[list-list-connect-append]
Thm* For any graph A,B:V List. A = B A-- > *B	[list-list-connect_weakening]
Thm* For any graph A,B:V List. B A A-- > *B	[list-list-connect-iseg]
Thm* For any graph A:V List, x:V. A-- > *[x] A-- > *x	[list-list-connect-singleton]
Thm* For any graph A,B,C:V List. A-- > *B B-- > *C A-- > *C	[list-list-connect_transitivity]

Try larger context: Graphs