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

At: mapoutl is singleton 1 1
1. A: Type
2. B: Type
3. L: (A+B) List
4. a: A
nil = [a] (L1,L2:(A+B) List. nil = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil)
By: Obvious
Generated subgoals:

None

About:
listconsconsnilunioninluniverseequalimpliesandexists

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