PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: equal appends case2
T:Type, x1,z,x2,x3:T List. ||z||||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2))
By:
Auto
THEN
Inst Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3)) [T;z;x1;x3;x2]
Generated subgoals:

None

About:
listuniverseequalimpliesandallexists

PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc