lemma funcset_id by Jeremy Avigad

--- a/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:31:27 2009 +0200
+++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:31:28 2009 +0200
@@ -63,6 +63,9 @@
 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
   by (simp add: Pi_def)
 
+lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
+  by (auto intro: Pi_I)
+
 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
   by (simp add: Pi_def)