Def  is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x

is mentioned by

Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,c,b:, e:({a..b}A). Thm*  (ac Thm*  ( Thm*  (c<b Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) Thm*  (= Thm*  (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))	[iter_via_intseg_split_pluck]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,b:, c:{a...b}, d:{c..b}, e:({a..b}A). Thm*  ((i:{a..b}. i<c  di  e(i) = u) Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))	[iter_via_intseg_amputate_units]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,c,b:, e:({a..b}A). Thm*  (ac Thm*  ( Thm*  (cb Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) Thm*  (= Thm*  (f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i)))	[iter_via_intseg_split_mid]
Thm*  f:(AAA), u:A. Thm*  is_commutative_sep(A; f) Thm*   Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,b:, e,g:({a..b}A). Thm*  (f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i)) Thm*  (= Thm*  ((Iter(f;u) i:{a..b}. f(e(i),g(i))) Thm*  ( A)	[iter_via_intseg_comp_binop]
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)	[iter_via_intseg_all_units]
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))	[iter_via_intseg_singleton]
Thm*  is_ident(; (x,y. x+y); 0)	[natadd_ident_zero]
Thm*  is_ident(; (x,y. x+y); 0)	[intadd_ident_zero]
Thm*  is_ident(; (x,y. xy); 1)	[natmul_ident_one]
Thm*  is_ident(; (x,y. xy); 1)	[intmul_ident_one]
Thm*  f:(AAA), u,v:A. is_ident(A; f; u)  is_ident(A; f; v)  u = v	[binary_ident_unique]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html