theory Type_Preservation imports "HOL-Nominal.Nominal" begin text ‹ This theory shows how to prove the type preservation property for the simply-typed lambda-calculus and beta-reduction. ›