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.
xv.P(x) 
(x:{x:T| x(eq) v }. P(x))10.
xv.P(x) (x:{x:T| x(eq) v }. P(x))11. P(u)
if eq(u,u)
true
else u(eq) v fi}
Type
xv.P(x) (x:{x:T| x(eq) v }. P(x))
xv.P(x) (x:{x:T| x(eq) v }. P(x))
if eq(u,u) true else u(eq) v fi
| 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. xv.P(x) (x:{x:T| x(eq) v }. P(x))10. xv.P(x) (x:{x:T| x(eq) v }. P(x))11. P(u) if eq(u,u) true else u(eq) v fi |
About:
 |  |  |  |
 |  |  |  |  |
 |