1. A : Type
2. B : Type
  f:((A+B)(i:2if i=0 A else B fi)),
  g:((i:2if i=0 A else B fi)(A+B)).
  InvFuns(A+B;i:2if i=0 A else B fi;f;g)

By:	Witness: union_to_sigma | sigma_to_union THEN BackThru:  Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)

None

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