This repository contains a formal proof of the type soundness of the Simply Typed Lambda Calculus (STLC) using Coq. The proof demonstrates that well-typed terms satisfy progress (a term is either a value or can take a step) and preservation (evaluation preserves types).