Type5. L: T List
6. u: T
7. v: T List
8.
x
v.P(x) 
(x:{x:T| x(eq) v }. P(x))9.
xv.P(x) 
(x:{x:T| x(eq) v }. P(x))10. x: T
11. if eq(x,u)
true
else x(eq) v fi12. P(x)
13. eq(x,u)
x = u
Dec(x = u)}
TT
x,y:T. eq(x,y) x = y
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 | 4. P: TType 5. L: T List 6. u: T 7. v: T List 8. xv.P(x) (x:{x:T| x(eq) v }. P(x))9. xv.P(x) (x:{x:T| x(eq) v }. P(x))10. x: T 11. if eq(x,u) true else x(eq) v fi12. P(x) 13. eq(x,u) x = u Dec(x = u) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |