At:
path-tl
1
2
2
1.
the_graph: Graph
2.
p: Vertices(the_graph) List
3.
1 < ||p||
4.
path(the_graph;p)
5.
q: Vertices(the_graph) List
6.
tl(p) = q
7.
i: 
(||p||-1)
i < ||q||
By:
RevHypSubst -2 0
THEN
RWO
Thm* 
l:A List. ||l||
1 
||tl(l)|| = ||l||-1 
0
Generated subgoals:
None
About:
