Progress lemma induction on term, instead of has_ty. Erased "closed 0 v" requirement from s_run_0.