diff -r dffffe36344a -r 7a1f285cad25 src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Sun Feb 28 18:33:57 2010 -0800
+++ b/src/HOLCF/Representable.thy	Sun Feb 28 19:39:50 2010 -0800
@@ -180,6 +180,18 @@
   shows "abs\<cdot>(rep\<cdot>x) = x"
 unfolding abs_def rep_def by (simp add: REP [symmetric])
 
+lemma deflation_abs_rep:
+  fixes abs and rep and d
+  assumes REP: "REP('b) = REP('a)"
+  assumes abs_def: "abs \<equiv> (coerce :: 'a \<rightarrow> 'b)"
+  assumes rep_def: "rep \<equiv> (coerce :: 'b \<rightarrow> 'a)"
+  shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+unfolding abs_def rep_def 
+apply (rule ep_pair.deflation_e_d_p)
+apply (rule ep_pair_coerce, simp add: REP)
+apply assumption
+done
+
 
 subsection {* Proving a subtype is representable *}