2. s: T List
3. z: T
4. (z
nil)
s1,s2:T List. nil = (s1 @ [z / s2])2. s: T List
3. u: T
4. v: T List
5.
z:T. (z v) 
(s1,s2:T List. v = (s1 @ [z / s2]))6. z: T
7. (z
[u / v]) s1,s2:T List. [u / v] = (s1 @ [z / s2])
T:Type, s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]))
| 1 | 1. T: Type 2. s: T List 3. z: T 4. (z nil) s1,s2:T List. nil = (s1 @ [z / s2]) | 1 step |
| 2 | 1. T: Type 2. s: T List 3. u: T 4. v: T List 5. z:T. (z v) (s1,s2:T List. v = (s1 @ [z / s2]))6. z: T 7. (z [u / v]) s1,s2:T List. [u / v] = (s1 @ [z / s2]) | 3 steps |
About:
 |  |  |  |  |  |  |  |