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