--- a/src/HOL/Lifting.thy Fri Sep 27 08:59:22 2013 +0200
+++ b/src/HOL/Lifting.thy Fri Sep 27 09:07:45 2013 +0200
@@ -76,6 +76,16 @@
lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
+lemma [simp]:
+ shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+ and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+by(auto simp add: left_unique_def right_unique_def)
+
+lemma [simp]:
+ shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
+ and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+by(simp_all add: left_total_def right_total_def)
+
subsection {* Quotient Predicate *}
definition