--- a/Nominal/Test.thy	Mon Mar 15 06:11:35 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 08:28:10 2010 +0100
@@ -28,14 +28,20 @@
 term "supp (x :: lam)"
 lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
+(* maybe should be added to Infinite.thy *)
 lemma infinite_Un:
   shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-apply(auto)
-done
+  by simp
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-sorry
+apply(induct b rule: lam_bp_inducts(2))
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp add: lam_bp_bn lam_bp_perm)
+apply(simp add: eqvts)
+done
 
 lemma supp_fv:
   "supp t = fv_lam t" and