2. P: T
Prop3. L: T List
x
L.P(x) 
(M,N:T List, x:T. P(x) & L = (M @ (x.N)))
T:Type, P:(TProp), L:T List. xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N)))
| 1 | 1. T: Type 2. P: T Prop3. L: T List xL.P(x) (M,N:T List, x:T. P(x) & L = (M @ (x.N))) |
About:
 |  |  |  |  |  |  |  |  |