(16steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sum family singleton elim 1
1. A : Type
2. a : A
3. B : {x:A| x = a }Type
  (i:{x:A| x = a }B(i)) ~ B(a)
By: (ib.ib/i,b. b)  (i:{x:A| x = a  A }B(i))B(a)  Asserted
THEN
Witness: ib.ib/i,b. b | b.<a,b>

Generated subgoals:

1   (ib.ib/i,b. b)  (i:{x:A| x = a }B(i))B(a)
5 steps
2 4. (ib.ib/i,b. b)  (i:{x:A| x = a }B(i))B(a)
  InvFuns(i:{x:A| x = a }B(i);B(a);ib.ib/i,b. b;b.<a,b>)
9 steps

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

(16steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc