e:({a..b
}
). (
i:{a..b}. e(i)) = 1 
(i:{a..b}. e(i) = 1)a,b:
, P:({a..b}Prop). (i:{a..b}. P(i)) (And i:{a..b}. P(i))f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b
a 
(Iter(f;u) i:{a..b}. e(i)) = uf:(AAA), u:A, a,b:, e:({a..b}A).
Thm* a<b
Thm*
Thm* (Iter(f;u) i:{a..b
}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))x,y:. x
y = 1 x = 1 & y = 1f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b
a (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{a..a}. e(i))