diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Jul 16 12:02:06 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Jul 16 12:09:48 1999 +0200
@@ -62,6 +62,18 @@
 by (Blast_tac 1);
 qed "UN_o";
 
+(** lemma for proving injectivity of representation functions for **)
+(** datatypes involving function types                            **)
+
+Goalw [o_def]
+  "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
+br ext 1;
+be allE 1;
+be allE 1;
+be mp 1;
+be fun_cong 1;
+qed "inj_fun_lemma";
+
 
 section "inj";
 (**NB: inj now just translates to inj_on**)
@@ -106,6 +118,11 @@
 by (rtac (rangeI RS minor) 1);
 qed "inj_transfer";
 
+Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
+by (rtac ext 1);
+by (etac injD 1);
+by (etac fun_cong 1);
+qed "inj_o";
 
 (*** inj_on f A: f is one-to-one over A ***)