--- a/Nominal/Ex/Lambda_add.thy	Wed Mar 02 12:49:01 2011 +0900
+++ b/Nominal/Ex/Lambda_add.thy	Wed Mar 02 16:07:56 2011 +0900
@@ -128,6 +128,24 @@
   by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1))
 
 
+definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx"
+
+lemma Lam_I : "\<II> = Lam[x]. Var x"
+  by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
+     (metis Rep_name_inverse atom_name_def fresh_at_base)
+
+definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)"
+definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)"
+
+lemma c1_c2[simp]:
+  "c1 \<noteq> c2"
+  unfolding c1_def c2_def
+  by (simp add: Abs_name_inject)
+
+definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2"
+lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y"
+  by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base)
+     (metis Rep_name_inverse atom_name_def fresh_at_base)
 
 end