(3steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul via intseg singleton 1

1. a : 
2. b : 
3. e : {a..b}
4. a+1 = b
  ( i:{a..b}. e(i)) = e(a)


By: BackThru: 
Thm*  f:(AAA), u:A.
Thm*  is_ident(Afu)
Thm*  
Thm*  (a,b:e:({a..b}A). a+1 = b  (Iter(f;ui:{a..b}. e(i)) = e(a))


Generated subgoal:

1   is_ident(; (x,yxy); 1)
1 step

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

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