Dot7.dfy: Dot6 with relaxed subtyping wfe-conditions, and full expression of subst lemma.