1. a : 
2. b : 
3. c : {a...b}
4. B : {a..b}Type
  (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))

By:	Inst:  Thm*  B:(AType), P:(AProp). Thm*  (i:A. Dec(P(i))) Thm*   Thm*  ((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i)))) Using:[A:= {a..b} | B:= B | P(i):= i<c] THEN Rewrite by Hyp:-1

1

5. (i:{a..b}B(i)) ~ ((i:{i:{a..b}| i<c }B(i))+(i:{i:{a..b}| i<c }B(i)))   ((i:{i:{a..b}| i<c }B(i))+(i:{i:{a..b}| i<c }B(i)))   ~   ((i:{a..c}B(i))+(i:{c..b}B(i)))

3 steps

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