Prop5. L: T List
6. u: T
7. v: T List
8. (
z:T. z(
eq) v 
P(z)) xv.P(x)9.
z:T. z(eq) (u.v) P(z)10. (eq(u,u))
(u = u)
if eq(u,u)
true
else u(eq) v fi}
TT
x,y:T. eq(x,y) x = y
Prop
z:T. z(eq) v P(z)) xv.P(x)
z:T. z(eq) (u.v) P(z)
if eq(u,u) true else u(eq) v fi
| 1 | 4. P: TProp 5. L: T List 6. u: T 7. v: T List 8. ( z:T. z(eq) v P(z)) xv.P(x)9. z:T. z(eq) (u.v) P(z)10. (eq(u,u)) (u = u) if eq(u,u) true else u(eq) v fi |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |