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

At: l before decomp 1 1
1. T: Type
2. L: T List
x,y:T. [x; y] nil (A,B:T List. nil = (A @ B) & (x A) & (y B))
By: RWO Thm* x:T, L:T List. [x / L] nil False 0
Generated subgoals:

None

About:
listconsconsniluniverseequal
impliesandfalseallexists

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