2. eq: {T=
}3. P: T
Prop4. L: T List
x
L.P(x) 
(z:T. z(eq) L 
P(z))
T:Type, eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z))
| 1 | 1. T: Type 2. eq: {T= }3. P: T Prop4. L: T List xL.P(x) (z:T. z(eq) L P(z)) |
About:
 |  |  |  |  |  |  |