--- a/Nominal/Ex/SingleLet.thy	Tue Jul 13 23:39:39 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Wed Jul 14 21:30:52 2010 +0100
@@ -21,12 +21,39 @@
 where
   "bn (As x y t) = {atom x}"
 
+typ trm
+typ assg
 term Var 
 term App
 term Baz
 term bn
 term fv_trm
 
+lemma [quot_respect]: 
+  "(op =  ===> alpha_trm_raw) Var_raw Var_raw"
+  "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw"
+apply(auto)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(assumption)
+apply(assumption)
+done
+
+
+
+lemma "Var x \<noteq> App y1 y2"
+apply(descending)
+apply(simp add: trm_raw.distinct)
+
+
+
+ML {*
+  map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.distinct(1)}
+*}
+
+
+
 
 typ trm
 typ assg