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