A,B,C:Type, f:(B inj
C), g:(A inj B). f o g 
A inj C
Inj(B; C; f) Inj(A; C; f o g)| Theorem | Name |
| A,B,C:Type, f:(B inj C), g:(A inj B). f o g A inj C | [compose_wf_inj] |
| cites the following: | |
| Inj(B; C; f) Inj(A; C; f o g) | [comp_preserves_inj] |