(23steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card split prod intseg family decbl 1 1 1
1. A : Type
2. B : AType
3. P : AProp
4. d : A2
5. x:A. if d(x)=0 P(x) else P(x) fi
  g:((x:A st P(x)B(x))(x:A st P(x)B(x))(x:AB(x))). 
  InvFuns(x:AB(x);(x:A st P(x)B(x))(x:A st P(x)B(x));h.<h,h>;g)
By: Witness:
Wifg,x. if d(x)=0 (fg/f,g. f)(x) else (fg/f,g. g)(x) fi
Wiwith type (x:A st P(x)B(x))(x:A st P(x)B(x))(x:AB(x))

Generated subgoals:

1   (fg,x. if d(x)=0 (fg/f,g. f)(x) else (fg/f,g. g)(x) fi)
   (x:A st P(x)B(x))(x:A st P(x)B(x))(x:AB(x))
3 steps
2 6. (fg,x. if d(x)=0 (fg/f,g. f)(x) else (fg/f,g. g)(x) fi)
6.  (x:A st P(x)B(x))(x:A st P(x)B(x))(x:AB(x))
  InvFuns(x:AB(x);(x:A st P(x)B(x))(x:A st P(x)B(x))
  InvFuns;h.<h,h>;fg,x. if d(x)=0 (fg/f,g. f)(x) else (fg/f,g. g)(x) fi)
16 steps

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

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