Proving correctness of an AVL-Tree colouring algorithm
You are recursing structurally, so you might want structural induction, but in AVL trees structural induction and induction on height are similar. You probably want to prove something a bit stronger than you need at the end - perhaps something like "AVL trees with height n return RB trees with black height n, and if n is even then neither child of the root is colored red."