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(A; f; u) Thm*   Thm*  (a,b:, e:({a..b}A). a+1 = b  (Iter(f;u) i:{a..b}. e(i)) = e(a))

1

is_ident(; (x,y. x+y); 0)

1 step

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