author | mengj |
Thu, 25 May 2006 08:07:02 +0200 | |
changeset 19717 | 2742cec21579 |
child 20645 | 5e28b8f2cb52 |
permissions | -rw-r--r-- |
%ID: $Id$ %Author: Jia Meng, NICTA %extensionality for partial types clause( forall([A, B, F, G], or( not(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))), a18 ).