T
3. (
x,y:T. eq(x,y) 
x = y) & eq 
TT4. P: T
Prop5. x: T
6. L: T List
x(eq) L 
P(x) 
yL.P(y)
}
Prop
x(eq) L P(x) yL.P(y)
| 1 | 2. eq: TT 3. ( x,y:T. eq(x,y) x = y) & eq TT4. P: T Prop5. x: T 6. L: T List x(eq) L P(x) yL.P(y) |
About:
 |  |  |  |  |  |