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

Auto
THEN
FwdThru Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3)) [-1]
THEN
ExRepD

1

1. T: Type 2. x1: T List 3. z: T List 4. x2: T List 5. x3: T List 6. ||x1|| = ||z|| 7. (x1 @ x2) = (z @ x3) 8. z': T List 9. z = (x1 @ z') 10. x2 = (z' @ x3) x1 = z & x2 = x3

4 steps

About: