(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 2
1. A : Type
2. B : Type
3. i : 2
4. e1 : if i=0 A else B fi
5. i = 1
  if i=0 inl(e1) else inr(e1) fi  A+B
By: Subst4: Hyp:5 THEN Reduce 4

Generated subgoal:

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

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

(6steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc