T
T
4.
x,y:T. eq(x,y) 
x = y5. P: T
Type6. L: T List
7. u: T
8. v: T List
9. (
x:{x:T| x(eq) v }. P(x)) 
xv.P(x)10. eq(u,u) = false
u(eq) v}
Type
x:{x:T| x(eq) v }. P(x)) xv.P(x)
u(eq) v
| 1 | 3. eq TT 4. x,y:T. eq(x,y) x = y5. P: T Type6. L: T List 7. u: T 8. v: T List 9. ( x:{x:T| x(eq) v }. P(x)) xv.P(x)10. eq(u,u) = false u(eq) v |
About:
 |  |  |  |  |  |  |  |  |  |  |