got rid of final assume in sel case of subst lemma