(11steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
l
member
decomp2
2
1
1
1.
T:
Type
2.
x,y:T. Dec(x = y)
3.
s:
T List
4.
u:
T
5.
v:
T List
6.
z:T. (z
v)
(
s1,s2:T List. v = (s1 @ [z / s2]) &
(z
s1))
7.
z:
T
8.
(z
[u / v])
9.
z = u
[u / v] = [z / v]
By:
Analyze
Generated subgoals:
None
About:
(11steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc