2. x: T List
3. y: T List
4. z: T List
5. (x @ z) = (y @ z)
x = y2. x: T List
3. y: T List
4. z: T List
5. x = y
(x @ z) = (y @ z)
T:Type, x,y,z:T List. (x @ z) = (y @ z) 
x = y
| 1 | 1. T: Type 2. x: T List 3. y: T List 4. z: T List 5. (x @ z) = (y @ z) x = y | 1 step |
| 2 | 1. T: Type 2. x: T List 3. y: T List 4. z: T List 5. x = y (x @ z) = (y @ z) | 1 step |
About:
 |  |  |  |