Nuprl - Proof: l member decomp 2 1

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

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

By: InstConcl [nil;v] THEN Reduce 0 THEN Analyze

Generated subgoals:

None

About: