(2steps total) PrintForm core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists functionality wrt implies
  S,T:Type, P,Q:(SProp).
  S = T  (x:S. P(x)  Q(x))  (x:S. P(x))  (y:T. Q(y))
By: Unfold `guard` 0 THEN UnivCD

Generated subgoal:

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

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

(2steps total) PrintForm core StandardLIB Doc