This is a follow-up for Li-yao Xia's answer on my StackOverflow question
Thanks for your answer Li-yao! I have a couple of follow-up notes/questions:
A Fixpoint on terms indexed by function types A -> B is useless since no subterms of any Select term are indexed by function types. For the same reason, induction is useless on such terms.