S,T:Type. (
n:
. n ~ S) & (n:. n ~ T) 
(n:. n ~ (S
T)) S,T:Type.
(n:, f:(nS). Bij(n; S; f)) & (n:, f:(nT). Bij(n; T; f))
(n:, f:(nST). Bij(n; ST; f))f:(AB). Bij(A; B; f)) 
(A ~ B))
0| 1 | S,T:Type. (n:. n ~ S) & (n:. n ~ T) (n:. n ~ (ST)) |
About:
 |  |  |  |  |  |  |