(4steps total) PrintForm Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: every wf 1
1. 'a : Type
2. p : 'a
3. l : 'a List
  every(p;l)  
By: Last ListInd

Generated subgoals:

1   every(p;nil)  
1 step
2 4. u : 'a
5. v : 'a List
6. every(p;v)  
  every(p;cons(u; v))  
1 step

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

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