1 header {* Definition of Lambda terms and convertibility *}

     1 header {* Definition of Lambda terms and convertibility *}

     2 

     2 

     4 

     4 

     5 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"

     5 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"

     6   unfolding fresh_def by blast

     6   unfolding fresh_def by blast

     7 

     7 

     8 atom_decl var

     8 atom_decl var