223 

   223 

   224 declare [[coercion "atom::var1\<Rightarrow>atom"]]

   224 declare [[coercion "atom::var1\<Rightarrow>atom"]]

   225 

   225 

   226 declare [[coercion "atom::var2\<Rightarrow>atom"]]

   226 declare [[coercion "atom::var2\<Rightarrow>atom"]]

   227 

   227 

   228 lemma

   229 lemma

   229   fixes a::"var1" and b::"var2"

   230   fixes a::"var1" and b::"var2"

   230   shows "a \<sharp> t \<and> b \<sharp> t"

   231   shows "a \<sharp> t \<and> b \<sharp> t"

   231 oops

   232 oops

   232 

   234 

   233 (* does not yet work: it needs image as

   235 (* does not yet work: it needs image as

   234    coercion map *)

   236    coercion map *)

   235 

   237 

   236 lemma

   238 lemma