Nuprl - Proof: union sigma inverses

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

A,B:Type.

InvFuns(A+B;i:

if i=

A else B fi;union_to_sigma;sigma_to_union)

By:

Auto

Generated subgoal:

1 1. A : Type
2. B : Type
InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)
6 steps

About:

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