(5steps total) Remark PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: add via intseg addends 4

1. a,b:e,g:({a..b}).
1. (x,yx+y)(( i:{a..b}. e(i)), i:{a..b}. g(i))
1. =
1. ( i:{a..b}. (x,yx+y)(e(i),g(i)))
  a,b:f,g:({a..b}).
  ( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))


By: Reduce Hyp:-1


Generated subgoals:

None

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

(5steps total) Remark PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc