--- a/Nominal/Ex/Lambda.thy	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 04 09:39:23 2013 +0100
@@ -4,6 +4,11 @@
   "~~/src/HOL/Library/Monad_Syntax"
 begin
 
+lemma perm_commute: 
+  "a \<sharp> p \<Longrightarrow> a' \<sharp> p \<Longrightarrow> (a \<rightleftharpoons> a') + p = p + (a \<rightleftharpoons> a')"
+apply(rule plus_perm_eq)
+apply(simp add: supp_swap fresh_def)
+done
 
 atom_decl name
 
@@ -14,6 +19,8 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+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)"
   unfolding alpha_lam_raw_def
   by perm_simp rule
@@ -378,6 +385,8 @@
   avoids b4: "x"
   by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
+thm beta.strong_induct
+
 text {* One-Reduction *}
 
 inductive