--- a/Nominal/Abs.thy	Thu May 06 14:14:30 2010 +0200
+++ b/Nominal/Abs.thy	Mon May 10 15:44:49 2010 +0200
@@ -840,5 +840,14 @@
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
+lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+  by auto
+
+lemma [eqvt]: "(p \<bullet> prod_rel A B x y) = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  by (simp, perm_simp) (rule refl)
+
+lemma [eqvt]: "(p \<bullet> prod_fv A B (x, y)) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  by (simp, perm_simp) (rule refl)
+
 end