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

At: l disjoint cons 3
1. T: Type
2. a: T List
3. b: T List
4. t: T
5. (t b)
6. x:T. ((x a) & (x b))
7. x: T
(x = t (x a) & (x b))
By: Obvious
Generated subgoals:

None

About:
listuniverseequalandorall

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