Nuprl - Proof: card union vs sigma

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card union vs sigma

A,B:Type. (A+B) ~ (i:

if i=

A else B fi)

By:	Def of <type> ~ <type>

Generated subgoal:

1 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)
1 step

About:

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