diff -r ff938c7b15e8 -r 5e28b8f2cb52 src/HOL/Tools/atp-inputs/u_helper1.tptp
--- a/src/HOL/Tools/atp-inputs/u_helper1.tptp	Wed Sep 20 13:54:03 2006 +0200
+++ b/src/HOL/Tools/atp-inputs/u_helper1.tptp	Wed Sep 20 13:56:39 2006 +0200
@@ -1,8 +1,14 @@
 %ID: $Id$
 %Author: Jia Meng, NICTA
-%extensionality, untyped
+%functional equality and extensionality, untyped
+
+input_clause(a9,axiom,
+[--hBOOL(hAPP(hAPP(fequal,X),Y)),++equal(X,Y)]).
 
-input_clause(a18,axiom,
+input_clause(a10,axiom,
+[++hBOOL(hAPP(hAPP(fequal,X),Y)),--equal(X,Y)]).
+
+input_clause(a11,axiom,
 [--equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G))),
 ++equal(F,G)]).