src/HOL/Lifting.thy

--- a/src/HOL/Lifting.thy	Thu Feb 20 16:56:32 2014 +0100
+++ b/src/HOL/Lifting.thy	Thu Feb 20 16:56:33 2014 +0100
@@ -155,6 +155,10 @@
   using a unfolding Quotient_def
   by blast
 
+lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t"
+  using a unfolding Quotient_def
+  by blast
+
 lemma Quotient_rep_abs_fold_unmap: 
   assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
   shows "R (Rep' x') x"