src/HOL/Lifting_Product.thy
changeset 56526 58ac520db7ae
parent 56525 b5b6ad5dc2ae
child 58444 ed95293f14b6
--- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:32 2014 +0200
+++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:33 2014 +0200
@@ -8,6 +8,11 @@
 imports Lifting Basic_BNFs
 begin
 
+(* The following lemma can be deleted when product is added to FP sugar *)
+lemma prod_pred_inject [simp]:
+  "pred_prod P1 P2 (a, b) = (P1 a \<and> P2 b)"
+  unfolding pred_prod_def fun_eq_iff prod_set_simps by blast
+
 subsection {* Transfer rules for the Transfer package *}
 
 context