 Britton's lemma

In an HNN extension, every word containing a stable letter and having no pinch $t^{-1}ct$ or $td{t}^{-1}$ is nonidentity. In particular, the natural map from the base group to its HNN extension is injective.