wip on sel case of subst lemma
almost done sketching sel case of subst lemma