PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
list-connect-singleton
For any graph
i,j:V. [i]-- > *j
i-the_graph- > *j
By:
Unfold `list-connect` 0
THEN
RWO
Thm*
P:(T
Prop), x:T, L:T List. (
y
[x / L].P(y))
P(x)
(
y
L.P(y)) 0
THEN
RWO
Thm*
P:(T
Prop). (
x
nil.P(x))
False 0
THEN
SplitOrHyps
THEN
Obvious
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
For any graph
i,j:V. [i]-- > *j 
i-the_graph- > *j
P:(T
Prop), x:T, L:T List. (
y
[x / L].P(y)) P(x) 
(yL.P(y))
0
P:(TProp). (xnil.P(x)) False
0