(2steps total) PrintForm core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all functionality wrt implies 1
1. S : Type
2. T : Type
3. P : SProp
4. Q : SProp
5. S = T
6. z:S. P(z)  Q(z)
7. x:S. P(x)
8. y : T
  Q(y)
By: HypBackchain

Generated subgoals:

None

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

(2steps total) PrintForm core StandardLIB Doc