--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp-inputs/par_helper1.tptp	Fri Apr 28 06:05:19 2006 +0200
@@ -0,0 +1,9 @@
+%ID: $Id$
+%Author: Jia Meng, NICTA
+%extensionality for partial types
+
+input_clause(a18,axiom,
+[--equal(hAPP(F,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B)),hAPP(G,hAPP(hAPP(hEXTENT,F,tc_fun(tc_fun(A,B),tc_fun(tc_fun(A,B),A))),G,tc_fun(tc_fun(A,B),A)),tc_fun(A,B))),
+++equal(F,G)]).
+
+