2 imports "../Nominal2" 

     2 imports "../Nominal2" 

     3 begin

     3 begin

     4 

     4 

     5 section {* The Weakening property in the simply-typed lambda-calculus *}

     5 section {* The Weakening property in the simply-typed lambda-calculus *}

     6 

     6