Induction on Variants

So far we've proved the correctness of recursive functions on natural numbers. We can do correctness proofs about recursive functions on variant types, too. That requires us to figure out how induction works on variants. We'll do that, next, starting with a variant type for representing natural numbers, then generalizing to lists, trees, and other variantss.