--- a/Nominal/Nominal2_Eqvt.thy	Mon Jan 10 11:36:55 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Thu Jan 13 12:12:47 2011 +0000
@@ -195,6 +195,16 @@
   unfolding Compl_eq_Diff_UNIV
   by (perm_simp) (rule refl)
 
+lemma subset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+  unfolding subset_eq
+  by (perm_simp) (rule refl)
+
+lemma psubset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+  unfolding psubset_eq
+  by (perm_simp) (rule refl)
+
 lemma image_eqvt:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
   unfolding permute_set_eq_image