It is interesting to discuss briefly also how one can define higher order relation induction and relation co-induction.
This is essentially the different nature with respect to the previous one, because this essentially the kind of induction that goes on in relation induction simply stams from the inductive definition of a given predicate. If this predicate is a minimal fix point, like if you want to describe a transition relation, or a maximal fix point, that is if you want to describe an observation relation, here you have realise an induction and co-induction principle.
So, as you see, these two inductive principles are nearely the logical expansion of the very definition of the predicates.