prove t_walkstar_ind

looks like a short proof, but was very tricky to come by. i think the
issue is that infer_t terms have lists of infer_t terms embedded inside
them whereas terms only have pairs, so we have to be explicit, when
reusing the term-based induction theorem, about what to do with lists.