1. A : Type
2. P : AProp
3. x:A. !i:2. if i=0 P(x) else P(x) fi
4. A ~ (i:2{x:A| if i=0 P(x) else P(x) fi })
  (i:2{x:A| if i=0 P(x) else P(x) fi })
  ~
  (i:2if i=0 {x:A| P(x) } else {x:A| P(x) } fi)

By:	BackThru:  Thm*  B,B':(AType). (x:A. B(x) ~ B'(x))  ((x:AB(x)) ~ (x:AB'(x))) THEN CBV: {x:A| <*> }

1

5. i : 2   {x:A| if i=0 P(x) else P(x) fi }   ~   if i=0 {x:A| P(x) } else {x:A| P(x) } fi

1 step

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