2. Discrete{T}
3. eq: {T
}4. L: T List
5. M: T List
(L @ M)(
eq)(M @ L)2. Discrete{T}
3. eq: {T
}4. L: T List
5. M: T List
(M @ L)(eq)(L @ M)
T:Type. Discrete{T} 
(eq:{T}, L,M:T List. (L @ M)(~eq)(M @ L))
| 1 | 1. T: Type 2. Discrete{T} 3. eq: {T }4. L: T List 5. M: T List (L @ M)(eq)(M @ L) |
| 2 | 1. T: Type 2. Discrete{T} 3. eq: {T }4. L: T List 5. M: T List (M @ L)(eq)(L @ M) |
About:
 |  |  |  |