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