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

At: mapoutl is append 1 1
1. A: Type
2. B: Type
3. l1: A List
4. l2: A List
L:(A+B) List. mapoutl(L) = l2 (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = nil & mapoutl(L2) = l2)
By:
Auto
THEN
InstConcl [nil;L]
THEN
Reduce 0
Generated subgoals:

None

About:
listnilunionuniverseequalimpliesandallexists

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