A:Type, b:, P,Q:(AProp).
  {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi

By:	SimilarTo Thm*  {x:A| if b P(x) else Q(x) fi } Thm*  =ext Thm*  if b {x:A| P(x) } else {x:A| Q(x) } fi

1

1. A : Type 2. b :  3. P : AProp 4. Q : AProp 5. {x:A| if b P(x) else Q(x) fi } =ext if b {x:A| P(x) } else {x:A| Q(x) } fi   {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi

1 step

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