(3steps total) PrintForm Definitions core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: not over exists

  T:Type, Q:(TProp). (x:TQ(x))  (x:TQ(x))

By: GenRepD


Generated subgoals:

1 1. T : Type
2. Q : TProp
3. (x:TQ(x))
4. x : T
  Q(x)

1 step
2 1. T : Type
2. Q : TProp
3. x:TQ(x)
  (x:TQ(x))

1 step

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

(3steps total) PrintForm Definitions core StandardLIB Doc