'c,'b,'a:S, f:('a
'c), g:('b'c).
Thm* (
h:(('a+'b)'c). (x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x)))
Thm* & (
h,y:(('a+'b)'c).
Thm* & ((
x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x))
Thm* & (& (
x:'a. y(inl(x)) = f(x))
Thm* & (& (
x:'b. y(inr(x)) = g(x))
Thm* & (
Thm* & (h = y)
'c,'b,'a:S.
Thm* all
Thm* (
f:'a 'c. all
Thm* (
f:'a 'c. (g:'b 'c. exists_unique
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. and
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. (all
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. equal
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. (h(inl(x))
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ((x:'a. ,f(x)))
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,all
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. equal
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. (h(inr(x))
Thm* (
f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,(x:'b. ,g(x)))))))