# Injection

## Definition

Fun.inj_def: inj ?f = ($$\forall$$x y. ?f x = ?f y $$\longrightarrow$$ x = y)

THEOREM    The composition of two injective functions is injective.

Proof available