Cover sets are at the core of implicit induction proof techniques which keep the advantages of explicit induction and proof by consistency. Contextual cover sets are a generalized form of them since they can be generated also with the help of 'not yet certified' information that can be however soundly used in the deduction process. In a first step, we present an abstract inference system as our general framework to build implicit induction provers. Compared with other similar inference systems, the new soundness proof arguments allowed us to weaken the applicability conditions of the inference rules and augment their simplification capabilities. Contextual cover sets are implemented by (combinations of) reasoning modules that may have different reasoning domains or deduction methods other than induction. In a second step, we present a generic and sound integration schema of reasoning modules inside our framework. As a case study, we define a set of reasoning modules for conditional theories based on rewriting techniques and we define the inference system of $Spike$ in terms of them. Finally, we propose extensions of it by introducing new reasoning modules for linear arithmetic or based on semantic subsumption. We give as example the application of an extended version of $Spike$ to prove the correctness of the MJRTY algorithm by performing a combination of inductive and arithmetic reasoning.