author | mengj |
Fri, 28 Apr 2006 06:05:19 +0200 | |
changeset 19492 | 29c6cba140da |
child 20645 | 5e28b8f2cb52 |
permissions | -rw-r--r-- |
%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)]).