PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: or via exist intseg split last
  a,b:, P:({a..b}Prop).
  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))
By: UnivCD
THEN
Inst: 
Thm*  a,b:, P:({a..b}Prop).
Thm*  a<b
Thm*  
Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))
Using:[a | b | P | b-1]

Generated subgoals:

None

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

PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc