--- a/Nominal/Ex/Lambda.thy	Mon Mar 24 15:31:17 2014 +0000
+++ b/Nominal/Ex/Lambda.thy	Sun Apr 06 13:07:24 2014 +0100
@@ -19,6 +19,39 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+lemma 
+  "Lam [x]. Var x = Lam [y]. Var y"
+proof -
+  obtain c::name where fresh: "atom c \<sharp> (Lam [x]. Var x, Lam [y]. Var y)"
+    by (metis obtain_fresh)
+  have "Lam [x]. Var x = (c \<leftrightarrow> x) \<bullet> Lam [x]. Var x"
+    using fresh by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: fresh_Pair)
+  also have "... = Lam [c].Var c" by simp
+  also have "... = (c \<leftrightarrow> y) \<bullet> Lam [c]. Var c"
+    using fresh by (rule_tac flip_fresh_fresh[symmetric]) (auto simp add: fresh_Pair)
+  also have "... = Lam [y]. Var y" by simp
+  finally show "Lam [x]. Var x = Lam [y]. Var y" .
+qed
+
+definition 
+  Name :: "nat \<Rightarrow> name" 
+where 
+  "Name n = Abs_name (Atom (Sort ''name'' []) n)"
+
+definition
+   "Ident2 = Lam [Name 1].(Var (Name 1))"
+
+definition 
+   "Ident x = Lam [x].(Var x)"
+
+lemma "Ident2 = Ident x"
+unfolding Ident_def Ident2_def
+by simp
+
+lemma "Ident x = Ident y"
+unfolding Ident_def
+by simp
+
 thm lam.strong_induct
 
 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
@@ -45,6 +78,7 @@
   "is_app (Var x) = False"
 | "is_app (App t1 t2) = True"
 | "is_app (Lam [x]. t) = False"
+thm is_app_graph_def is_app_graph_aux_def
 apply(simp add: eqvt_def is_app_graph_aux_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)