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

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

1

is_ident(; (x,y. xy); 1)

1 step

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