T:Type, a,c,b,d:T List. (a @ b) = (c @ d) (e:T List. a = (c @ e) & d = (e @ b) c = (a @ e) & b = (e @ d))

1	1. T: Type 2. a: T List c,b,d:T List. b = (c @ d) (e:T List. nil = (c @ e) & d = (e @ b) c = e & b = (e @ d))	1 step
2	1. T: Type 2. a: T List 3. u: T 4. v: T List 5. c,b,d:T List. (v @ b) = (c @ d) (e:T List. v = (c @ e) & d = (e @ b) c = (v @ e) & b = (e @ d)) c,b,d:T List. [u / (v @ b)] = (c @ d) (e:T List. [u / v] = (c @ e) & d = (e @ b) c = [u / (v @ e)] & b = (e @ d))	3 steps

About: