(3steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
assert-member-left-paren
1
1
1.
T:
Type
2.
E:
T
T
3.
x,y:T. E(x,y)
x = y
4.
i:
T
5.
s:
(T+T) List
6.
i1:
||s||
7.
x1:
T
8.
s[i1] = inl(x1)
9.
E(x1,i)
i@0:
. i@0 < ||s|| & inl(i) = s[i@0]
By:
Obvious
Generated subgoals:
None
About:
(3steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
T
x,y:T. E(x,y) 
x = y
||s||
i@0:. i@0 < ||s|| & inl(i) = s[i@0]
