(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: equal append front 1
1. T: Type
2. x: T List
3. y: T List
4. z: T List
5. (x @ z) = (y @ z)
x = y
By:
Inst Thm* x1,z,x2,x3:T List. ||x1|| = ||z|| (x1 @ x2) = (z @ x3) x1 = z & x2 = x3 [T;x;y;z;z]
THEN
ApFunToHypEquands `q' ||q|| -1
THEN
RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| -1
Generated subgoals:

None

About:
listintadduniverseequalimpliesandall

(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc