--- a/Nominal/Ex/Lambda.thy	Mon Nov 07 13:58:18 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Tue Nov 08 22:31:31 2011 +0000
@@ -12,6 +12,22 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
+  unfolding alpha_lam_raw_def
+  by perm_simp rule
+
+lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
+proof -
+  have "alpha_lam_raw (rep_lam (abs_lam t)) t"
+    using rep_abs_rsp_left Quotient_lam equivp_reflp lam_equivp by metis
+  then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
+    unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
+  then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
+    using Quotient_rel Quotient_lam by metis
+  thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
+qed
+
+
 section {* Simple examples from Norrish 2004 *}
 
 nominal_primrec