T:Type, x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3))

1	1. T: Type 2. x1: T List z,x2,x3:T List. 0||z|| x2 = (z @ x3) (z':T List. z = z' & x2 = (z' @ x3))	1 step
2	1. T: Type 2. x1: T List 3. u: T 4. v: T List 5. z,x2,x3:T List. ||v||||z|| (v @ x2) = (z @ x3) (z':T List. z = (v @ z') & x2 = (z' @ x3)) z,x2,x3:T List. ||v||+1||z|| [u / (v @ x2)] = (z @ x3) (z':T List. z = [u / (v @ z')] & x2 = (z' @ x3))	6 steps

About: