--- a/Nominal/Ex/Lambda.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Mar 22 12:18:30 2016 +0000
@@ -72,23 +72,6 @@
 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)"
-  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 Quotient3_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 Quotient3_rel Quotient3_lam by metis
-  thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
-qed
-
 
 section {* Simple examples from Norrish 2004 *}