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

At: equal appends case1 2 1
1. T: Type
2. x1: T List
3. u: T
4. v: T List
5. z,x2,x3:T List. ||v||||z|| (v @ x2) = (z @ x3) (z':T List. z = (v @ z') & x2 = (z' @ x3))
6. z: T List
x2,x3:T List. ||v||+10 [u / (v @ x2)] = x3 (z':T List. nil = [u / (v @ z')] & x2 = (z' @ x3))
By: Obvious
Generated subgoals:

None

About:
listconsnilnatural_numberadduniverse
equalimpliesandallexists

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