In this extended abstract, we present a method for structuring type soundness proofs in Dafny to improve proof stability. As a case study, we apply the method to proving type soundness for a small expression language, and demonstrate empirically how it improves resource usage metrics known to correlate with stability. Our method can scale to realistic proofs, as demonstrated by its use in the type soundness proof of the Cedar language.