--- 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"