# HG changeset patch
# User urbanc
# Date 1146845393 -7200
# Node ID 63e18ed22fdaa5ee5bb000ad51b816dadc99eea6
# Parent  67d1792dc0f208ddd210d31d9e0986b86ece24e1
added the lemma pt_fresh_bij2

diff -r 67d1792dc0f2 -r 63e18ed22fda src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri May 05 17:38:26 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri May 05 18:09:53 2006 +0200
@@ -1351,6 +1351,16 @@
   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
 using a by (simp add: pt_fresh_bij[OF pt, OF at])
 
+lemma pt_fresh_bij2:
+  fixes  pi :: "'x prm"
+  and     x :: "'a"
+  and     a :: "'x"
+  assumes pt: "pt TYPE('a) TYPE('x)"
+  and     at: "at TYPE('x)"
+  and     a:  "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
+  shows  "a\<sharp>x"
+using a by (simp add: pt_fresh_bij[OF pt, OF at])
+
 lemma pt_perm_fresh1:
   fixes a :: "'x"
   and   b :: "'x"