(2steps total) PrintForm Definitions mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iseg map
  A,B:Type, f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)
By: Unfold `iseg` 0 THEN ExRepD THEN HypSubst -1 0

Generated subgoal:

1 1. A : Type
2. B : Type
3. f : AB
4. L1 : A List
5. L2 : A List
6. l : A List
7. L2 = (L1 @ l)
  l@0:B List. map(f;L1 @ l) = (map(f;L1) @ l@0)
1 step

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

(2steps total) PrintForm Definitions mb list 2 Sections MarkB generic Doc