(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: finite-type-iff-list
  T:Type. finite-type(T)  (L:T List. x:T. (x  L))
By: Unfold `finite-type` 0 THEN ExRepD

Generated subgoals:

1 1. T : Type
2. n : 
3. f : nT
4. Surj(n; T; f)
  L:T List. x:T. (x  L)
4 steps
2 1. T : Type
2. L : T List
3. x:T. (x  L)
  n:, f:(nT). Surj(n; T; f)
2 steps

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

(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Search Doc