--- a/src/HOL/Library/Quotient_Set.thy Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Sat Sep 10 22:43:17 2011 +0200
@@ -76,10 +76,20 @@
lemma mem_prs[quot_preserve]:
assumes "Quotient R Abs Rep"
+ shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
+using Quotient_abs_rep[OF assms]
+by(simp add: fun_eq_iff mem_def)
+
+lemma mem_rsp[quot_respect]:
+ "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
+ by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
+
+lemma mem_prs2:
+ assumes "Quotient R Abs Rep"
shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
-lemma mem_rsp[quot_respect]:
+lemma mem_rsp2:
shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
by (intro fun_relI) (simp add: set_rel_def)