While it is possible to use rule or erule with the generated .induct theorem from a datatype, it is usually much simpler and more convenient to use the induct proof method. Similar to the case_tac method, apply (induct t) splits the goal into various cases, one for each constructor of the type of t. The difference is that for recursive cases of the datatype, we also get an inductive hypothesis added to our assumptions.