(2steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eval factorization split mid

  a,c,b:f:({a..b}).
  ac  cb  {a..b}(f) = {a..c}(f){c..b}(f)


By: Def of {<int>..<int>}(f)


Generated subgoal:

1 1. a : 
2. c : 
3. b : 
4. f : {a..b}
5. ac
6. cb
  ( i:{a..b}. if(i)) = ( i:{a..c}. if(i))( i:{c..b}. if(i))

1 step

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

(2steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc