Nuprl - Pf list all all 1 1

At: list all all 1 1

1. T: Type
2. eq: {T=}
3. P: TType
4. L: T List
5. xL.P(x)
6. x: {x:T| x(eq) L }

P(x)

By: Using [`T',T;`eq',eq;`z',x] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [-2])

Generated subgoals:

1 x(eq) L

2 7. P(x)
P(x)

About: