stlc-norm F* proof that STLC is normalizing by Yannick Forster, Lukas Krämer, and Franziska Müller (Saarland University)