At:
l member decomp2221
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
(z v)
By:
RWO
Thm*l:T List, a,x:T. (x [a / l]) x = a (x l)
-2
THEN
Analyze -2
Generated subgoals:
x,y:T. Dec(x = y)
v) 
(
s1,s2:T List. v = (s1 @ [z / s2]) & 
(z 
(z 
(x