(6steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: intseg split 1 1 1 2

1. a : 
2. b : 
3. c : {a...b}
4. {a..b} ~ ({x:{a..b}| x<c }+{x:{a..b}| x<c })
  {c..b} =ext {x:{a..b}| x<c }


By: Analyze


Generated subgoals:

None

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

(6steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc