Start by fixing Phi and w, and assuming the hypotheses of the rule.
Since check works by structural recursion on t, let's do induction on t.
In fact, if I was feeling extra moral, I'd say let's do recursion induction on check, effectively using elimination wrt the implementation to justify elimination wrt the specification. Of course, recursion induction on check is just structural recursion on t wrapped up and specifically labelled as `the induction which allows one step of computation'. This is good design, as it removes the apparent coincidence by which induction on the data seems to work.
Next: induction on t | Prev: check's elim rule | Up: contents