(5steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: map wf listp 1 1 1
1. A : Type
2. B : Type
3. f : AB
4. l : A List
5. ||l||1
  0<||map(f;l)||
By: RWW Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||   0

Generated subgoal:

1   0<||l||
1 step

About:
listassertintnatural_numberfunctionuniverseequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(5steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc