(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
  A,B:Type. sigma_to_union  (i:2if i=0 A else B fi)(A+B)
By: UnivCD THEN Def of sigma_to_union THEN Analyze THEN Analyze3 THEN Reduce Concl

Generated subgoal:

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
5 steps

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

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc