(4steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A choice principle.

At: ax choice version3

  A,B:Type, Q:(ABProp).
  (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))
By: Auto

Generated subgoals:

1 1. A : Type
2. B : Type
3. Q : ABProp
4. x:A. y:B. Q(x,y)
  f:(AB). x:A. Q(x,f(x))
1 step
2 1. A : Type
2. B : Type
3. Q : ABProp
4. f:(AB). x:A. Q(x,f(x))
5. x : A
  y:B. Q(x,y)
2 steps

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

(4steps total) PrintForm Definitions Lemmas LogicSupplement Sections DiscrMathExt Doc