At:
dfl-traversal-connect
For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 dfl-traversal(the_graph;L2;s) dfl-traversal(the_graph;L1;s)
By:
(Auto THEN (ParallelOp -1) THEN ExRepD THEN SplitAndConcl THEN (Try Trivial)) THENL [(ParallelOp -2) THEN (ParallelOp -1) THEN ExRepD;(RepeatFor 5 (ParallelOp -1)) THEN ExRepD]
THEN
All (RWO "list-list-connect-singleton < ")
THEN
Using [`B',L2]
(BackThru
Thm* For any graph
A,B,C:V List. A-- > *B B-- > *C A-- > *C)
Generated subgoals:
For any graph
L1,L2:V List, s:Traversal. L1-- > *L2 
dfl-traversal(the_graph;L2;s)