(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sigma to union wf 1

1. A : Type
2. B : Type
3. i : 2
4. e1 : if i=0 A else B fi
  if i=0 inl(e1) else inr(e1) fi  A+B


By: IntSegElim 3


Generated subgoals:

1 5. i = 0  2
  if i=0 inl(e1) else inr(e1) fi  A+B

2 steps
2 5. i = 1  2
  if i=0 inl(e1) else inr(e1) fi  A+B

2 steps

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

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc