Wrote a mathematical proof
Learned Type Theory
Proving Type Soundness In A Simply Typed Lambda Calculus
Evaluation contexts, typing rules, runtime semantic rules, and type soundness for a simply-typed lambda calculus with various traditional language features.
https://nickzuber.com/pdf/type-soundness.pdf