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

At: l before append iff 1 1
1. T: Type
2. A: T List
3. B: T List
4. x: T
5. y: T
6. B': T List
7. [x; y] = B'
8. nil A
9. B' B
[x; y] A [x; y] B (x A) & (y B)
By: Obvious
Generated subgoals:

None

About:
listconsniluniverseequalandor

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