(3steps total) PrintForm Definitions core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists functionality wrt iff
  S,T:Type, P,Q:(SProp).
  S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))
By: GenUnivCD

Generated subgoals:

1 1. S : Type
2. T : Type
3. P : SProp
4. Q : SProp
5. S = T
6. x:S. P(x)  Q(x)
7. x:S. P(x)
  y:T. Q(y)
1 step
2 1. S : Type
2. T : Type
3. P : SProp
4. Q : SProp
5. S = T
6. x:S. P(x)  Q(x)
7. y:T. Q(y)
  x:S. P(x)
1 step

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

(3steps total) PrintForm Definitions core StandardLIB Doc