Nuprl - Pf list all is member nil lemma

T:Type, eq:(TT), L:T List. xL.x(eq) nil nil = L

By: UnivCD THEN Analyze 0

Generated subgoals:

1 1. T: Type
2. eq: TT
3. L: T List
xL.x(eq) nil nil = L

2 1. T: Type
2. eq: TT
3. L: T List
xL.x(eq) nil (nil = L)

About:

1	1. `T:` `Type` 2. `eq:` `TT` 3. `L:` `T List` `xL.x(eq) nil nil = L`
2	1. `T:` `Type` 2. `eq:` `TT` 3. `L:` `T List` `xL.x(eq) nil (nil = L)`