diff -r 992db37acead -r 8e0ff1bfcfea src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Thu Sep 12 15:22:52 1996 +0200
+++ b/src/HOLCF/Cfun2.ML	Thu Sep 12 17:18:00 1996 +0200
@@ -111,6 +111,13 @@
         ]);
 
 
+qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
+	cut_facts_tac prems 1,
+	rtac (eq_UU_iff RS iffD2) 1,
+	etac subst 1,
+	rtac (minimal RS monofun_cfun_arg) 1]);
+
+
 (* ------------------------------------------------------------------------ *)
 (* ch2ch - rules for the type 'a -> 'b                                      *)
 (* use MF2 lemmas from Cont.ML                                              *)