(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 2

1. 'a : Type
2. p : 'a
3. 'a List
4. u : 'a
5. v : 'a List
6. every(p;v 
  every(p;cons(uv))  


By: RecUnfold `every` 0 THEN Reduce 0 THEN Simp


Generated subgoals:

None

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