(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select wf

  A:Type, l:A List, n:. 0n  n<||l||  l[n A

By: UnivCD


Generated subgoal:

1 1. A : Type
2. l : A List
3. n : 
4. 0n
5. n<||l||
  l[n A

4 steps

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

(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc