src/HOL/Lifting.thy
changeset 47889 29212a4bb866
parent 47777 f29e7dcd7c40
child 47936 756f30eac792
--- a/src/HOL/Lifting.thy	Fri May 04 11:08:31 2012 +0200
+++ b/src/HOL/Lifting.thy	Fri May 04 17:12:37 2012 +0200
@@ -310,6 +310,9 @@
 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
 
+lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
+  using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
+
 end
 
 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}