T
T
4. P: T
Prop5. L: T List
6. u: T
7. v: T List
8.
yv.P(y) 
(x:T. x(eq) v & P(x))9. P(u)
10. eq(u,u)
u = u
if eq(u,u)
true
else u(eq) v fiT
x,y:T. eq(x,y) x = y
TT
Prop
yv.P(y) (x:T. x(eq) v & P(x))
if eq(u,u) true else u(eq) v fi
| 1 | 3. eq TT 4. P: T Prop5. L: T List 6. u: T 7. v: T List 8. yv.P(y) (x:T. x(eq) v & P(x))9. P(u) 10. eq(u,u) u = u if eq(u,u) true else u(eq) v fi |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |