T
T
4.
x,y:T. eq(x,y) 
x = y5. P: T
Prop6. L: T List
7.
xL.P(x)8. z: T
9. z(
eq) L
P(z) TT4.
x,y:T. eq(x,y) x = y5. P: T
Prop6. L: T List
7.
z:T. z(eq) L 
P(z) xL.P(x)
}
Prop
xL.P(x) (z:T. z(eq) L P(z))
| 1 | 3. eq TT 4. x,y:T. eq(x,y) x = y5. P: T Prop6. L: T List 7. xL.P(x)8. z: T 9. z( eq) L P(z) |
| 2 | 3. eq TT 4. x,y:T. eq(x,y) x = y5. P: T Prop6. L: T List 7. z:T. z(eq) L P(z) xL.P(x) |
About:
 |  |  |  |  |  |  |