src/HOL/Tools/atp-inputs/u_helper1.dfg

real_norm_def [simp]

%ID: $Id$
%Author: Jia Meng, NICTA
%functional equality and extensionality, untyped

clause(
forall([X, Y],
or( not(hBOOL(hAPP(hAPP(fequal,X),Y))),
    equal(X,Y))),
a9 ).

clause(
forall([X, Y],
or( not(equal(X,Y)),
    hBOOL(hAPP(hAPP(fequal,X),Y)))),
a10 ).

clause(
forall([F, G],
or( not(equal(hAPP(F,hAPP(hAPP(hEXTENT,F),G)),hAPP(G,hAPP(hAPP(hEXTENT,F),G)))),
    equal(F,G))),
a11 ).