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