f:(A
AA), 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)P:(Prop).
Thm* (
a:, b:{...a}. P(a,b))
Thm*
Thm* (
a:. (b:{...a}. P(a,b)) (b:{a...}. P(a,b))) (a,b:. P(a,b))f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* b
a (Iter(f;u) i:{a..b}. e(i)) = uP:(Prop), a:.
Thm* (
b:{a...}. (c:{a..b}. P(a,c)) P(a,b)) (b:{a...}. P(a,b))f:(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))