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

At: append is singleton 2 2
1. T: Type
2. a: T List
3. u: T
4. v: T List
5. b:T List, x:T. [x] = (v @ b) v = nil & b = [x] b = nil & v = [x]
6. b: T List
7. x: T
8. x = u
9. nil = (v @ b)
[u / v] = [x]
By:
Analyze
THEN
Obvious
Generated subgoals:

None

About:
listconsconsniluniverseequalimpliesandorall

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