--- a/LamEx.thy	Fri Oct 30 15:52:47 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 16:35:43 2009 +0100
@@ -167,15 +167,50 @@
 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
 
-ML {* lift_thm_lam @{context} @{thm pi_var_com} *}
-ML {* lift_thm_lam @{context} @{thm pi_app_com} *}
-ML {* lift_thm_lam @{context} @{thm pi_lam_com} *}
+ML {* val pi_var = lift_thm_lam @{context} @{thm pi_var_com} *}
+ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *}
+ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *}
+
+ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *}
+ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *}
+ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
+
+ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
+ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
+ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
+
+
+local_setup {*
+  Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
+  Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
+  Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #>
+  Quotient.note (@{binding "a1"}, a1) #> snd #>
+  Quotient.note (@{binding "a2"}, a2) #> snd #>
+  Quotient.note (@{binding "a3"}, a3) #> snd
+*}
 
-ML {* lift_thm_lam @{context} @{thm rfv_var} *}
-ML {* lift_thm_lam @{context} @{thm rfv_app} *}
-ML {* lift_thm_lam @{context} @{thm rfv_lam} *}
+thm alpha.cases
+
+thm rlam.inject
+thm pi_var
+
+lemma var_inject:
+  shows "(Var a = Var b) = (a = b)"
+sorry
 
-ML {* lift_thm_lam @{context} @{thm a3} *}
+lemma var_supp:
+  shows "supp (Var a) = ((supp a)::name set)"
+  apply(simp add: supp_def)
+  apply(simp add: pi_var)
+  apply(simp add: var_inject)
+  done
+
+lemma var_fresh:
+  fixes a::"name"
+  shows "(a\<sharp>(Var b)) = (a\<sharp>b)"
+  apply(simp add: fresh_def)
+  apply(simp add: var_supp)
+  done