"induction" instead of "destruct"

This is a version of Vladimir's pull request #37 that compiles.  I'll close that pull request.