k:
, f:(k inj
k). 
i:
. u:k. f{
i}(u) = uk:, f:(k inj k), u:k. i:. f{i}(u) = uk:, Q:(k
AProp).
Thm* (
x:k. y:A. Q(x;y)) 
(f:(kA). x:k. Q(x;f(x)))a,b:
, e:({a..b
}), i:{a..b}. e(i) | (
i:{a..b}. e(i))a,b:. a | b 
(c:. b = a
c)x,y:. xy 
x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) Af:(AA), u:A. f(u) = u (i:. f{i}(u) = u)