From F to DOT: Type Soundness Proofs with Definitional Interpreters