x,y,z:T List. (x @ z) = (y @ z) 
x = yas,bs:T List. ||as @ bs|| = ||as||+||bs|| 
x1,z,x2,x3:T List. ||x1|| = ||z|| 
(x1 @ x2) = (z @ x3) x1 = z & x2 = x3| Rank | Theorem | Name |
| 2 | Thm* x,y,z:T List. (x @ z) = (y @ z) x = y | [equal_append_front] |
| cites | ||
| 0 | Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |
| 1 | Thm* x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3 | [equal_appends_eq] |