(9steps total) Gloss PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc type poly mem const 1
1. f : D:Type. D(D List)
2. A : Type
3. a : A
4. x : A
  x list f(a)  x = a
By: Auto

Generated subgoals:

1 5. x list f(a)
  x = a
5 steps
2   f(a)  A List
2 steps

About:
listisectapplyfunctionuniverseequalmemberimplies
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) Gloss PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Search Doc