Nuprl - Pf is member non nil

T:Type, eq:{T=}, u:T, L:T List. u(eq) L (v:T, M:T List. L = v.M)

By: Analyze 0 THEN Analyze 0 THEN DiscreteEq -1 THEN UnivCD

Generated subgoal:

1 1. T: Type
2. eq: {T=}
3. eq TT
4. x,y:T. eq(x,y) x = y
5. u: T
6. L: T List
7. u(eq) L
v:T, M:T List. L = v.M

About: