(12steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all intseg vs iter and 1

1. a : 
  b:P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))


By: b:P:({a..b}Prop). ba  ((i:{a..b}. P(i))  (And i:{a..b}. P(i))) |
k:b:.
b-a = k  (P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i)))
Asserted


Generated subgoals:

1   b:P:({a..b}Prop). ba  ((i:{a..b}. P(i))  (And i:{a..b}. P(i)))
2 steps
2 2. b:P:({a..b}Prop). ba  ((i:{a..b}. P(i))  (And i:{a..b}. P(i)))
  k:b:.
  b-a = k  (P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i)))

4 steps
3 2. b:P:({a..b}Prop). ba  ((i:{a..b}. P(i))  (And i:{a..b}. P(i)))
3. k:b:.
3. b-a = k  (P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i)))
  b:P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))

4 steps

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

(12steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc