PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
list-list-connect-singleton
For any graph
A:V List, x:V. A-- > *[x]
A-- > *x
By:
Unfold `list-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
BackThru
Thm*
P:(T
Prop). (
x
nil.P(x))
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
For any graph
A:V List, x:V. A-- > *[x] 
A-- > *x
P:(T
Prop), x:T, L:T List. (y
[x / L].P(y)) P(x) & (yL.P(y))
0
P:(TProp). (xnil.P(x))