added some helper files for HOL goals/lemmas. Clauses have TPTP format.
%ID: $Id$
%Author: Jia Meng, NICTA
%extensionality for const-types-only
input_clause(a18,axiom,
[--equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G))),
++equal(F,G)]).