(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: partition type 1 1 2

1. A : Type
2. B : Type
3. P : ABProp
4. x:A!y:BP(x;y)
5. f : AB
6. x:AP(x;f(x))
  InvFuns(A;y:B{x:AP(x;y) };x.<f(x),x>;yx.2of(yx))


By: Analyze THEN New:u Analyze THEN Reduce Concl


Generated subgoal:

1 7. u : y:B{x:AP(x;y) }
  <f(2of(u)),2of(u)> = u  y:B{x:AP(x;y) }

8 steps

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

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc