At:
l member decomp22
1.
T: Type
2.
s: T List
3.
u: T
4.
v: T List
5.
z:T. (z v) (s1,s2:T List. v = (s1 @ [z / s2]))
6.
z: T
7.
(z v) s1,s2:T List. [u / v] = (s1 @ [z / s2])
By:
FwdThru -3 [-1]
THEN
ExRepD
THEN
InstConcl [[u / s1];s2]
THEN
Reduce 0
THEN
Analyze
Generated subgoals:
z:T. (z 
v) 
(
s1,s2:T List. v = (s1 @ [z / s2]))
