At:
dfsl-traversal-nil
1
2
1.
the_graph: Graph
2.
i: Vertices(the_graph)
3.
s1: (Vertices(the_graph)+Vertices(the_graph)) List
4.
s2: (Vertices(the_graph)+Vertices(the_graph)) List
5.
j:Vertices(the_graph). i-the_graph- > *j 
non-trivial-loop(the_graph;j)
6.
nil = (s1 @ [inl(i)] @ s2)
7.
j: Vertices(the_graph)
8.
i-the_graph- > *j
(inr(j) 
s2)
By:
ObviousContradiction [6]
Generated subgoals:
None
About:
