Writing an inductive proof...