Nuprl - Proof: sigma to union wf 1 1 1

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

1. A : Type
2. B : Type
3. i :

2
4. e1 : A
5. i = 0

if i=

inl(e1) else inr(e1) fi

A+B

By:	SplitITE Concl

Generated subgoals:

None

About:

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