At:
assert-member-paren
1
2
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.
y: T
8.
s[i1] = inr(y)
9.
E(y,i)
(
i@0:. i@0 < ||s|| & inl(i) = s[i@0]) 
(i@0:. i@0 < ||s|| & inr(i) = s[i@0])
By:
Obvious
Generated subgoals:
None
About:
