Nuprl - Pf is member wf 1

1. T: Type
2. eq: TT
3. x: T
4. L: T List

x(eq) L

By: ListInd 4

Generated subgoals:

1 x(eq) nil

2 5. u: T
6. v: T List
7. x(eq) v
x(eq) (u.v)

About:

1	`x(eq) nil`
2	5. `u:` `T` 6. `v:` `T List` 7. `x(eq) v` `x(eq) (u.v)`