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

At: l before decomp 1 2 1 1
1. T: Type
2. L: T List
3. u: T
4. v: T List
5. x,y:T. [x; y] v (A,B:T List. v = (A @ B) & (x A) & (y B))
6. x: T
7. y: T
8. x = u
9. [y] v
(x [u])
By: RWO Thm* a,x:T. (x [a]) x = a 0
Generated subgoals:

None

About:
listconsniluniverseequalimpliesandallexists

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