Nuprl - Proof: l member decomp 2

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 [u / v])

s1,s2:T List. [u / v] = (s1 @ [z / s2])

By: RWO Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) -1 THEN SplitOrHyps

Generated subgoals:

1 7. z = u
s1,s2:T List. [u / v] = (s1 @ [z / s2]) 1 step

2 7. (z v)
s1,s2:T List. [u / v] = (s1 @ [z / s2]) 1 step

About: