(5steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
append
is
singleton
2
1
1.
T:
Type
2.
a:
T List
3.
u:
T
4.
v:
T List
5.
b:T List, x:T. [x] = (v @ b)
v = nil & b = [x]
b = nil & v = [x]
6.
b:
T List
7.
x:
T
8.
x = u
9.
nil = (v @ b)
b = nil
By:
Obvious
Generated subgoals:
None
About:
(5steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc