Inductive theorem proving combines equational reasoning and induction to prove properties on ground terms. We present some basics, and show how it also applies in data structures not having a unique representation and in infinite data structures.