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
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))
7. f : x:A st P(x)B(x)
8. g : x:A st P(x)B(x)
  <x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi
  ,x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi>
  =
  <f,g>

By:	(x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi)  x:AB(x) Asserted

1	(x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi)  x:AB(x)	4 steps
2	9. (x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi)  x:AB(x)   <x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi   ,x.if d(x)=0 (<f,g>/f,g. f)(x) else (<f,g>/f,g. g)(x) fi>   =   <f,g>    (x:A st P(x)B(x))(x:A st P(x)B(x))	6 steps

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