(7steps total) PrintForm Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: map2 wf 1
1. 'a : Type
2. 'b : Type
3. 'c : Type
4. f : 'a'b'c
5. l1 : 'a List
6. l2 : 'b List
  map2(f;l1;l2)  'c List
By: MoveToConcl 6 THEN Last ListInd THEN Simp THEN StrongAuto

Generated subgoals:

1   map2(f;nil;l2)  'c List
1 step
2 6. u : 'a
7. v : 'a List
8. l2:'b List. map2(f;v;l2)  'c List
9. l2 : 'b List
  map2(f;cons(u; v);l2)  'c List
4 steps

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

(7steps total) PrintForm Definitions hol list 1 Sections HOLlib Doc