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