x1,z,x2,x3:T List. ||z||
||x1|| 
(x1 @ x2) = (z @ x3) (
z':T List. x1 = (z @ z') & x3 = (z' @ x2))x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3))| Theorem | Name |
| Thm* x1,z,x2,x3:T List. ||z||||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2)) | [equal_appends_case2] |
| cites | |
| Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3)) | [equal_appends_case1] |