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

At: append one one 1 1
1. T: Type
2. x: T List
3. z: T List
4. y: T List
5. w: T List
6. ||x|| = ||z|| ||y|| = ||w||
7. (x @ y) = (z @ w)
8. x = (z @ nil) & w = (nil @ y) z = (x @ nil) & y = (nil @ w)
nil = nil T List
By: Obvious
Generated subgoals:

None

About:
listnilintuniverseequalandor

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