diff -r 52c22fccdaaf -r 2742cec21579 src/HOL/Tools/atp-inputs/u_helper1.dfg
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/u_helper1.dfg	Thu May 25 08:07:02 2006 +0200
@@ -0,0 +1,10 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%extensionality, untyped
+
+clause(
+forall([F, G],
+or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G)))),
+    equal(F,G))),
+a18 ).
+