(8steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: equal appends case1 1
1. T: Type
2. x1: T List
z,x2,x3:T List. 0||z|| x2 = (z @ x3) (z':T List. z = z' & x2 = (z' @ x3))
By:
Auto
THEN
Obvious
Generated subgoals:

None

About:
listnatural_numberuniverseequalimpliesandallexists

(8steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc