(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: list-connect-append
For any graph A,B:V List, i:V. A @ B-- > *i A-- > *i B-- > *i
By:
Unfold `list-connect` 0
THEN
Unfold `l_exists` 0
THEN
RWO Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) 0
Generated subgoals:

11. the_graph: Graph
2. A: Vertices(the_graph) List
3. B: Vertices(the_graph) List
4. i: Vertices(the_graph)
5. y:Vertices(the_graph). (y A) (y B) & y-the_graph- > *i
(y:Vertices(the_graph). (y A) & y-the_graph- > *i) (y:Vertices(the_graph). (y B) & y-the_graph- > *i)		1 step
 
21. the_graph: Graph
2. A: Vertices(the_graph) List
3. B: Vertices(the_graph) List
4. i: Vertices(the_graph)
5. (y:Vertices(the_graph). (y A) & y-the_graph- > *i) (y:Vertices(the_graph). (y B) & y-the_graph- > *i)
y:Vertices(the_graph). (y A) (y B) & y-the_graph- > *i		1 step

About:
listuniverseandorallexists

(3steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc