At:
l member decomp221
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 s1,s2:T List. [u / v] = (s1 @ [z / s2]) & (z s1)
By:
InstConcl [nil;v]
THEN
Reduce 0
Generated subgoals:
[u / v] = [z / v]
(z 
nil)
x,y:T. Dec(x = y)
(
s1,s2:T List. v = (s1 @ [z / s2]) & 
