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