--- a/Quot/Nominal/Abs.thy	Mon Feb 01 11:39:59 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 01 12:06:46 2010 +0100
@@ -62,6 +62,9 @@
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _")
 
+lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
+  by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
+
 lemma alpha_gen_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"