Def  sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi

is mentioned by

Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)

[union_sigma_inverses]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html