|T| == 
f:(S
T). Inj(S; T; f)
Thm* 
S,T:Type. |S| |T| 
Prop
a1,a2:A. f(a1) = f(a2) B 
a1 = a2
Thm* A,B:Type, f:(AB). Inj(A; B; f) Prop
| card_le |
Def |S| |T| == f:(ST). Inj(S; T; f)
Thm* |
| inject |
Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B a1 = a2
Thm* |
About:
 |  |  |  |  |
 |  |  |  |  |