First order inductive theorem proving deals with proving new equations based on a given set of equations. More specifically, we are interested in proving that the axioms logically imply the goals. In this presentation I will discuss how we can automate these proofs by induction. The equations can either describe finite or infinite terms. In this talk we are mainly interested in applying these ideas of induction on infinite objects. The focus is on the most simple form of infinite objects: infinite sequences of some basic data type. Using a special operator take we can also apply our induction techniques on infinite data. Finally we describe how our techniques can be implemented in practice.