src/HOL/Library/FuncSet.thy

   "compose A g f = (\<lambda>x\<in>A. g (f x))"
 
 
 subsection{*Basic Properties of @{term Pi}*}
 
-lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
+lemma Pi_I[simp]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
   by (simp add: Pi_def)
 
 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
   by (simp add: Pi_def)
 

 lemma Pi_empty [simp]: "Pi {} B = UNIV"
   by (simp add: Pi_def)
 
 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
   by (simp add: Pi_def)
-
+(*
+lemma funcset_id [simp]: "(%x. x): A -> A"
+  by (simp add: Pi_def)
+*)
 text{*Covariance of Pi-sets in their second argument*}
 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
   by (simp add: Pi_def, blast)
 
 text{*Contravariance of Pi-sets in their first argument*}