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

At: mapoutl is append
A,B:Type, L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2)
By:
Auto
THEN
ExRepD
Generated subgoals:

11. A: Type
2. B: Type
3. L: (A+B) List
4. l1: A List
5. l2: A List
6. mapoutl(L) = (l1 @ l2)
L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2		7 steps
 
21. A: Type
2. B: Type
3. L: (A+B) List
4. l1: A List
5. l2: A List
6. L1: (A+B) List
7. L2: (A+B) List
8. L = (L1 @ L2)
9. mapoutl(L1) = l1
10. mapoutl(L2) = l2
mapoutl(L) = (l1 @ l2)		1 step

About:
listunionuniverseequalandallexists

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