Nuprl - Some Definitions

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

	Some definitions of interest.

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

	Thm* A,B:Type. sigma_to_union (i:2if i=0 A else B fi)(A+B)

union_to_sigma	Def union_to_sigma(e) == InjCase(e; a. <0,a>; b. <1,b>)

	Thm* A,B:Type. union_to_sigma (A+B)(i:2if i=0 A else B fi)

About:

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