# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270137399 -7200
# Node ID 13d905f1999a323d40b21dbc3421faff8dfa6d03
# Parent  6bf14c13c2915b76b3853d60ccccabf87f575fa3# Parent  1ea57097ce129cf2a998d36c2425307bd073e5e3
merged

diff -r 6bf14c13c291 -r 13d905f1999a Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Apr 01 17:56:26 2010 +0200
+++ b/Nominal/ExLet.thy	Thu Apr 01 17:56:39 2010 +0200
@@ -92,6 +92,13 @@
   apply(simp_all add:permute_bn eqvts)
   done
 
+lemma fv_fv_bn:
+  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  by blast
+
 lemma Lt_subst:
   "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
   apply (simp only: trm_lts.eq_iff)