Search for blocks/addresses/...
Proofgold Asset
asset id
56e0c78fe3013d566f12bb30c14dc0de760e9094eb80d78697069ea8cbc3edbe
asset hash
6ae700ad519cb3c7085356877edd0123cf06a4547af6b5c5594c6ddc43a68db5
bday / block
39379
tx
4a721..
preasset
doc published by
Pr4zB..
Param
4402e..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
cf2df..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
Subq
Subq
:
ι
→
ι
→
ο
Param
setminus
setminus
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Param
5bab1..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
654b9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7e5de..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a3794..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
093ca..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
34ae8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
96162..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3c407..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d92ce..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
105be..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a2064..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f5da9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b9a4e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6e81c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4e91d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8c9ed..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
37e04..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
13b7c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2bf4d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
53286..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7db3a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
22587..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4d3d7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
de118..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b0749..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
54c7d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cf078..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b43ab..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
96c31..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
627df..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
74622..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3f98b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a0d70..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
dbf71..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f842a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
23b40..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d5d69..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2e1d5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
94f0c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
923e2..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1a9fd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b39ef..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0788d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e2ec9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
65996..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
45286..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8bd80..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
729bd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
76a6c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8d9b1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1668d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c4d5c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e37fb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e8ba7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7f17b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d2e51..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9eede..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
150dd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2c550..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
286f8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b8d2a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
05795..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
59a16..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cec27..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ba960..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c2e8a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
adf05..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
07c0f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b7a83..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
74a95..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fc090..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
72d65..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b7e1a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5024..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
91113..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f0823..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a9907..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4b4dd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a47b6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
aa358..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ee649..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
57f60..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a7e88..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
59632..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b1702..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f444d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a1497..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
858ba..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c480f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0db75..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
02471..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
30a11..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
093ad..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0768d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
70a3c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2122d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
61fc8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
39c17..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
496a0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
87273..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ed012..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b0e38..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d68bd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f3db6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b4c31..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1a9c5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
10d66..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f4940..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f630d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
49901..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fb26f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4086f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9a66e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d0e7c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a3d60..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3a6bc..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
228c9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1cf57..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
dc830..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ee5b5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ad740..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0e6b2..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a3e51..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
356c7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1e661..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9aef0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bfd4f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c705c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6e051..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
df50d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d0e1f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
95ba7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
176ba..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
62e18..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
803e1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d0980..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b19dd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
61b2a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9f93b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
30182..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
811c0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2eb4b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d2a2c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e1aab..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a94a5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
62ca1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bce5f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
38793..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a13f2..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
21189..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
292f7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d3446..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
abda1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
73f36..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5d8ad..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
14fa0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
94ee4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
92dea..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
de95d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bacd8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
858d1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cdde4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
79ee1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2bb2a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8be9f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7cafd..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
55a3e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8c70b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
17819..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
53f52..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
07fce..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
bc2c6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e13e5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
02d0f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
91ca0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9069f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fb47b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
241b0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8fbce..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3fca5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ef324..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4e4f8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1e021..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
724e0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a6296..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
989b4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6661c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ef237..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3c50c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5c8a3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
af5b6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f6312..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f96b5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2c7a3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2dbe7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
86fe8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fef36..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fa2d0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
23b03..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
682ac..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
78a44..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
93f0f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5063..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6348c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
27706..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2dac5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
06d7e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
055d9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4b18d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2ffc8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
05a8c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
u9
:
ι
Param
76e3a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
79529..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1b69c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c8a3f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
68de1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
263f9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ed1c7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
44fd1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
df026..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
23926..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
71ae3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
889b5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
06ba7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0076f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
43a9d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6bc75..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cc7e8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
255f4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f9a67..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u10
:=
ordsucc
u9
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
e2ea8..
:
∀ x0 x1 .
atleastp
(
ordsucc
x0
)
x1
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x1
)
(
atleastp
x0
(
setminus
x1
(
Sing
x3
)
)
)
⟶
x2
)
⟶
x2
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Known
a55d1..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
x0
⊆
x1
⟶
4402e..
x1
x2
⟶
4402e..
x0
x2
Known
setminus_Subq
setminus_Subq
:
∀ x0 x1 .
setminus
x0
x1
⊆
x0
Known
e7c7c..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
x0
⊆
x1
⟶
cf2df..
x1
x2
⟶
cf2df..
x0
x2
Known
e79db..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
76e3a..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
aba88..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
79529..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
732af..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
1b69c..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
b44d9..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
c8a3f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
d38ac..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
68de1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
7b4b0..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
263f9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
f43e6..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
ed1c7..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
65a22..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
44fd1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
eb420..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
df026..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
6ef3d..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
23926..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
84c45..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
71ae3..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
46936..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
889b5..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
7daf4..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
06ba7..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
58605..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
0076f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
02ebd..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
43a9d..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
0c026..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
6bc75..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
37e36..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
cc7e8..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
cc30c..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
255f4..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
cfa25..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
f9a67..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
⟶
∀ x13 : ο .
x13
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Theorem
58b70..
:
∀ x0 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x5 .
x5
∈
x4
⟶
∀ x6 .
x6
∈
x4
⟶
∀ x7 .
x7
∈
x4
⟶
∀ x8 .
x8
∈
x4
⟶
∀ x9 .
x9
∈
x4
⟶
∀ x10 .
x10
∈
x4
⟶
∀ x11 .
x11
∈
x4
⟶
∀ x12 .
x12
∈
x4
⟶
∀ x13 .
x13
∈
x4
⟶
x0
x2
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
5bab1..
x1
x2
)
⟶
∀ x1 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x2 .
∀ x3 :
ι →
ι → ο
.
(
∀ x4 .
x4
∈
x2
⟶
∀ x5 .
x5
∈
x2
⟶
x3
x4
x5
⟶
x3
x5
x4
)
⟶
4402e..
x2
x3
⟶
cf2df..
x2
x3
⟶
∀ x4 .
x4
∈
x2
⟶
∀ x5 .
x5
⊆
setminus
x2
(
Sing
x4
)
⟶
∀ x6 .
x6
∈
x5
⟶
∀ x7 .
x7
∈
x5
⟶
∀ x8 .
x8
∈
x5
⟶
∀ x9 .
x9
∈
x5
⟶
∀ x10 .
x10
∈
x5
⟶
∀ x11 .
x11
∈
x5
⟶
∀ x12 .
x12
∈
x5
⟶
∀ x13 .
x13
∈
x5
⟶
∀ x14 .
x14
∈
x5
⟶
x1
x3
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
5bab1..
x2
x3
)
⟶
∀ x2 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x3 .
∀ x4 :
ι →
ι → ο
.
(
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
x4
x5
x6
⟶
x4
x6
x5
)
⟶
4402e..
x3
x4
⟶
cf2df..
x3
x4
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
⊆
setminus
x3
(
Sing
x5
)
⟶
∀ x7 .
x7
∈
x6
⟶
∀ x8 .
x8
∈
x6
⟶
∀ x9 .
x9
∈
x6
⟶
∀ x10 .
x10
∈
x6
⟶
∀ x11 .
x11
∈
x6
⟶
∀ x12 .
x12
∈
x6
⟶
∀ x13 .
x13
∈
x6
⟶
∀ x14 .
x14
∈
x6
⟶
∀ x15 .
x15
∈
x6
⟶
x2
x4
x7
x8
x9
x10
x11
x12
x13
x14
x15
⟶
5bab1..
x3
x4
)
⟶
∀ x3 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x4 .
∀ x5 :
ι →
ι → ο
.
(
∀ x6 .
x6
∈
x4
⟶
∀ x7 .
x7
∈
x4
⟶
x5
x6
x7
⟶
x5
x7
x6
)
⟶
4402e..
x4
x5
⟶
cf2df..
x4
x5
⟶
∀ x6 .
x6
∈
x4
⟶
∀ x7 .
x7
⊆
setminus
x4
(
Sing
x6
)
⟶
∀ x8 .
x8
∈
x7
⟶
∀ x9 .
x9
∈
x7
⟶
∀ x10 .
x10
∈
x7
⟶
∀ x11 .
x11
∈
x7
⟶
∀ x12 .
x12
∈
x7
⟶
∀ x13 .
x13
∈
x7
⟶
∀ x14 .
x14
∈
x7
⟶
∀ x15 .
x15
∈
x7
⟶
∀ x16 .
x16
∈
x7
⟶
x3
x5
x8
x9
x10
x11
x12
x13
x14
x15
x16
⟶
5bab1..
x4
x5
)
⟶
∀ x4 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x5 .
∀ x6 :
ι →
ι → ο
.
(
∀ x7 .
x7
∈
x5
⟶
∀ x8 .
x8
∈
x5
⟶
x6
x7
x8
⟶
x6
x8
x7
)
⟶
4402e..
x5
x6
⟶
cf2df..
x5
x6
⟶
∀ x7 .
x7
∈
x5
⟶
∀ x8 .
x8
⊆
setminus
x5
(
Sing
x7
)
⟶
∀ x9 .
x9
∈
x8
⟶
∀ x10 .
x10
∈
x8
⟶
∀ x11 .
x11
∈
x8
⟶
∀ x12 .
x12
∈
x8
⟶
∀ x13 .
x13
∈
x8
⟶
∀ x14 .
x14
∈
x8
⟶
∀ x15 .
x15
∈
x8
⟶
∀ x16 .
x16
∈
x8
⟶
∀ x17 .
x17
∈
x8
⟶
x4
x6
x9
x10
x11
x12
x13
x14
x15
x16
x17
⟶
5bab1..
x5
x6
)
⟶
∀ x5 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x6 .
∀ x7 :
ι →
ι → ο
.
(
∀ x8 .
x8
∈
x6
⟶
∀ x9 .
x9
∈
x6
⟶
x7
x8
x9
⟶
x7
x9
x8
)
⟶
4402e..
x6
x7
⟶
cf2df..
x6
x7
⟶
∀ x8 .
x8
∈
x6
⟶
∀ x9 .
x9
⊆
setminus
x6
(
Sing
x8
)
⟶
∀ x10 .
x10
∈
x9
⟶
∀ x11 .
x11
∈
x9
⟶
∀ x12 .
x12
∈
x9
⟶
∀ x13 .
x13
∈
x9
⟶
∀ x14 .
x14
∈
x9
⟶
∀ x15 .
x15
∈
x9
⟶
∀ x16 .
x16
∈
x9
⟶
∀ x17 .
x17
∈
x9
⟶
∀ x18 .
x18
∈
x9
⟶
x5
x7
x10
x11
x12
x13
x14
x15
x16
x17
x18
⟶
5bab1..
x6
x7
)
⟶
∀ x6 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x7 .
∀ x8 :
ι →
ι → ο
.
(
∀ x9 .
x9
∈
x7
⟶
∀ x10 .
x10
∈
x7
⟶
x8
x9
x10
⟶
x8
x10
x9
)
⟶
4402e..
x7
x8
⟶
cf2df..
x7
x8
⟶
∀ x9 .
x9
∈
x7
⟶
∀ x10 .
x10
⊆
setminus
x7
(
Sing
x9
)
⟶
∀ x11 .
x11
∈
x10
⟶
∀ x12 .
x12
∈
x10
⟶
∀ x13 .
x13
∈
x10
⟶
∀ x14 .
x14
∈
x10
⟶
∀ x15 .
x15
∈
x10
⟶
∀ x16 .
x16
∈
x10
⟶
∀ x17 .
x17
∈
x10
⟶
∀ x18 .
x18
∈
x10
⟶
∀ x19 .
x19
∈
x10
⟶
x6
x8
x11
x12
x13
x14
x15
x16
x17
x18
x19
⟶
5bab1..
x7
x8
)
⟶
∀ x7 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x8 .
∀ x9 :
ι →
ι → ο
.
(
∀ x10 .
x10
∈
x8
⟶
∀ x11 .
x11
∈
x8
⟶
x9
x10
x11
⟶
x9
x11
x10
)
⟶
4402e..
x8
x9
⟶
cf2df..
x8
x9
⟶
∀ x10 .
x10
∈
x8
⟶
∀ x11 .
x11
⊆
setminus
x8
(
Sing
x10
)
⟶
∀ x12 .
x12
∈
x11
⟶
∀ x13 .
x13
∈
x11
⟶
∀ x14 .
x14
∈
x11
⟶
∀ x15 .
x15
∈
x11
⟶
∀ x16 .
x16
∈
x11
⟶
∀ x17 .
x17
∈
x11
⟶
∀ x18 .
x18
∈
x11
⟶
∀ x19 .
x19
∈
x11
⟶
∀ x20 .
x20
∈
x11
⟶
x7
x9
x12
x13
x14
x15
x16
x17
x18
x19
x20
⟶
5bab1..
x8
x9
)
⟶
∀ x8 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x9 .
∀ x10 :
ι →
ι → ο
.
(
∀ x11 .
x11
∈
x9
⟶
∀ x12 .
x12
∈
x9
⟶
x10
x11
x12
⟶
x10
x12
x11
)
⟶
4402e..
x9
x10
⟶
cf2df..
x9
x10
⟶
∀ x11 .
x11
∈
x9
⟶
∀ x12 .
x12
⊆
setminus
x9
(
Sing
x11
)
⟶
∀ x13 .
x13
∈
x12
⟶
∀ x14 .
x14
∈
x12
⟶
∀ x15 .
x15
∈
x12
⟶
∀ x16 .
x16
∈
x12
⟶
∀ x17 .
x17
∈
x12
⟶
∀ x18 .
x18
∈
x12
⟶
∀ x19 .
x19
∈
x12
⟶
∀ x20 .
x20
∈
x12
⟶
∀ x21 .
x21
∈
x12
⟶
x8
x10
x13
x14
x15
x16
x17
x18
x19
x20
x21
⟶
5bab1..
x9
x10
)
⟶
∀ x9 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x10 .
∀ x11 :
ι →
ι → ο
.
(
∀ x12 .
x12
∈
x10
⟶
∀ x13 .
x13
∈
x10
⟶
x11
x12
x13
⟶
x11
x13
x12
)
⟶
4402e..
x10
x11
⟶
cf2df..
x10
x11
⟶
∀ x12 .
x12
∈
x10
⟶
∀ x13 .
x13
⊆
setminus
x10
(
Sing
x12
)
⟶
∀ x14 .
x14
∈
x13
⟶
∀ x15 .
x15
∈
x13
⟶
∀ x16 .
x16
∈
x13
⟶
∀ x17 .
x17
∈
x13
⟶
∀ x18 .
x18
∈
x13
⟶
∀ x19 .
x19
∈
x13
⟶
∀ x20 .
x20
∈
x13
⟶
∀ x21 .
x21
∈
x13
⟶
∀ x22 .
x22
∈
x13
⟶
x9
x11
x14
x15
x16
x17
x18
x19
x20
x21
x22
⟶
5bab1..
x10
x11
)
⟶
∀ x10 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x11 .
∀ x12 :
ι →
ι → ο
.
(
∀ x13 .
x13
∈
x11
⟶
∀ x14 .
x14
∈
x11
⟶
x12
x13
x14
⟶
x12
x14
x13
)
⟶
4402e..
x11
x12
⟶
cf2df..
x11
x12
⟶
∀ x13 .
x13
∈
x11
⟶
∀ x14 .
x14
⊆
setminus
x11
(
Sing
x13
)
⟶
∀ x15 .
x15
∈
x14
⟶
∀ x16 .
x16
∈
x14
⟶
∀ x17 .
x17
∈
x14
⟶
∀ x18 .
x18
∈
x14
⟶
∀ x19 .
x19
∈
x14
⟶
∀ x20 .
x20
∈
x14
⟶
∀ x21 .
x21
∈
x14
⟶
∀ x22 .
x22
∈
x14
⟶
∀ x23 .
x23
∈
x14
⟶
x10
x12
x15
x16
x17
x18
x19
x20
x21
x22
x23
⟶
5bab1..
x11
x12
)
⟶
∀ x11 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x12 .
∀ x13 :
ι →
ι → ο
.
(
∀ x14 .
x14
∈
x12
⟶
∀ x15 .
x15
∈
x12
⟶
x13
x14
x15
⟶
x13
x15
x14
)
⟶
4402e..
x12
x13
⟶
cf2df..
x12
x13
⟶
∀ x14 .
x14
∈
x12
⟶
∀ x15 .
x15
⊆
setminus
x12
(
Sing
x14
)
⟶
∀ x16 .
x16
∈
x15
⟶
∀ x17 .
x17
∈
x15
⟶
∀ x18 .
x18
∈
x15
⟶
∀ x19 .
x19
∈
x15
⟶
∀ x20 .
x20
∈
x15
⟶
∀ x21 .
x21
∈
x15
⟶
∀ x22 .
x22
∈
x15
⟶
∀ x23 .
x23
∈
x15
⟶
∀ x24 .
x24
∈
x15
⟶
x11
x13
x16
x17
x18
x19
x20
x21
x22
x23
x24
⟶
5bab1..
x12
x13
)
⟶
∀ x12 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x13 .
∀ x14 :
ι →
ι → ο
.
(
∀ x15 .
x15
∈
x13
⟶
∀ x16 .
x16
∈
x13
⟶
x14
x15
x16
⟶
x14
x16
x15
)
⟶
4402e..
x13
x14
⟶
cf2df..
x13
x14
⟶
∀ x15 .
x15
∈
x13
⟶
∀ x16 .
x16
⊆
setminus
x13
(
Sing
x15
)
⟶
∀ x17 .
x17
∈
x16
⟶
∀ x18 .
x18
∈
x16
⟶
∀ x19 .
x19
∈
x16
⟶
∀ x20 .
x20
∈
x16
⟶
∀ x21 .
x21
∈
x16
⟶
∀ x22 .
x22
∈
x16
⟶
∀ x23 .
x23
∈
x16
⟶
∀ x24 .
x24
∈
x16
⟶
∀ x25 .
x25
∈
x16
⟶
x12
x14
x17
x18
x19
x20
x21
x22
x23
x24
x25
⟶
5bab1..
x13
x14
)
⟶
∀ x13 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x14 .
∀ x15 :
ι →
ι → ο
.
(
∀ x16 .
x16
∈
x14
⟶
∀ x17 .
x17
∈
x14
⟶
x15
x16
x17
⟶
x15
x17
x16
)
⟶
4402e..
x14
x15
⟶
cf2df..
x14
x15
⟶
∀ x16 .
x16
∈
x14
⟶
∀ x17 .
x17
⊆
setminus
x14
(
Sing
x16
)
⟶
∀ x18 .
x18
∈
x17
⟶
∀ x19 .
x19
∈
x17
⟶
∀ x20 .
x20
∈
x17
⟶
∀ x21 .
x21
∈
x17
⟶
∀ x22 .
x22
∈
x17
⟶
∀ x23 .
x23
∈
x17
⟶
∀ x24 .
x24
∈
x17
⟶
∀ x25 .
x25
∈
x17
⟶
∀ x26 .
x26
∈
x17
⟶
x13
x15
x18
x19
x20
x21
x22
x23
x24
x25
x26
⟶
5bab1..
x14
x15
)
⟶
∀ x14 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x15 .
∀ x16 :
ι →
ι → ο
.
(
∀ x17 .
x17
∈
x15
⟶
∀ x18 .
x18
∈
x15
⟶
x16
x17
x18
⟶
x16
x18
x17
)
⟶
4402e..
x15
x16
⟶
cf2df..
x15
x16
⟶
∀ x17 .
x17
∈
x15
⟶
∀ x18 .
x18
⊆
setminus
x15
(
Sing
x17
)
⟶
∀ x19 .
x19
∈
x18
⟶
∀ x20 .
x20
∈
x18
⟶
∀ x21 .
x21
∈
x18
⟶
∀ x22 .
x22
∈
x18
⟶
∀ x23 .
x23
∈
x18
⟶
∀ x24 .
x24
∈
x18
⟶
∀ x25 .
x25
∈
x18
⟶
∀ x26 .
x26
∈
x18
⟶
∀ x27 .
x27
∈
x18
⟶
x14
x16
x19
x20
x21
x22
x23
x24
x25
x26
x27
⟶
5bab1..
x15
x16
)
⟶
∀ x15 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x16 .
∀ x17 :
ι →
ι → ο
.
(
∀ x18 .
x18
∈
x16
⟶
∀ x19 .
x19
∈
x16
⟶
x17
x18
x19
⟶
x17
x19
x18
)
⟶
4402e..
x16
x17
⟶
cf2df..
x16
x17
⟶
∀ x18 .
x18
∈
x16
⟶
∀ x19 .
x19
⊆
setminus
x16
(
Sing
x18
)
⟶
∀ x20 .
x20
∈
x19
⟶
∀ x21 .
x21
∈
x19
⟶
∀ x22 .
x22
∈
x19
⟶
∀ x23 .
x23
∈
x19
⟶
∀ x24 .
x24
∈
x19
⟶
∀ x25 .
x25
∈
x19
⟶
∀ x26 .
x26
∈
x19
⟶
∀ x27 .
x27
∈
x19
⟶
∀ x28 .
x28
∈
x19
⟶
x15
x17
x20
x21
x22
x23
x24
x25
x26
x27
x28
⟶
5bab1..
x16
x17
)
⟶
∀ x16 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x17 .
∀ x18 :
ι →
ι → ο
.
(
∀ x19 .
x19
∈
x17
⟶
∀ x20 .
x20
∈
x17
⟶
x18
x19
x20
⟶
x18
x20
x19
)
⟶
4402e..
x17
x18
⟶
cf2df..
x17
x18
⟶
∀ x19 .
x19
∈
x17
⟶
∀ x20 .
x20
⊆
setminus
x17
(
Sing
x19
)
⟶
∀ x21 .
x21
∈
x20
⟶
∀ x22 .
x22
∈
x20
⟶
∀ x23 .
x23
∈
x20
⟶
∀ x24 .
x24
∈
x20
⟶
∀ x25 .
x25
∈
x20
⟶
∀ x26 .
x26
∈
x20
⟶
∀ x27 .
x27
∈
x20
⟶
∀ x28 .
x28
∈
x20
⟶
∀ x29 .
x29
∈
x20
⟶
x16
x18
x21
x22
x23
x24
x25
x26
x27
x28
x29
⟶
5bab1..
x17
x18
)
⟶
∀ x17 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x18 .
∀ x19 :
ι →
ι → ο
.
(
∀ x20 .
x20
∈
x18
⟶
∀ x21 .
x21
∈
x18
⟶
x19
x20
x21
⟶
x19
x21
x20
)
⟶
4402e..
x18
x19
⟶
cf2df..
x18
x19
⟶
∀ x20 .
x20
∈
x18
⟶
∀ x21 .
x21
⊆
setminus
x18
(
Sing
x20
)
⟶
∀ x22 .
x22
∈
x21
⟶
∀ x23 .
x23
∈
x21
⟶
∀ x24 .
x24
∈
x21
⟶
∀ x25 .
x25
∈
x21
⟶
∀ x26 .
x26
∈
x21
⟶
∀ x27 .
x27
∈
x21
⟶
∀ x28 .
x28
∈
x21
⟶
∀ x29 .
x29
∈
x21
⟶
∀ x30 .
x30
∈
x21
⟶
x17
x19
x22
x23
x24
x25
x26
x27
x28
x29
x30
⟶
5bab1..
x18
x19
)
⟶
∀ x18 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x19 .
∀ x20 :
ι →
ι → ο
.
(
∀ x21 .
x21
∈
x19
⟶
∀ x22 .
x22
∈
x19
⟶
x20
x21
x22
⟶
x20
x22
x21
)
⟶
4402e..
x19
x20
⟶
cf2df..
x19
x20
⟶
∀ x21 .
x21
∈
x19
⟶
∀ x22 .
x22
⊆
setminus
x19
(
Sing
x21
)
⟶
∀ x23 .
x23
∈
x22
⟶
∀ x24 .
x24
∈
x22
⟶
∀ x25 .
x25
∈
x22
⟶
∀ x26 .
x26
∈
x22
⟶
∀ x27 .
x27
∈
x22
⟶
∀ x28 .
x28
∈
x22
⟶
∀ x29 .
x29
∈
x22
⟶
∀ x30 .
x30
∈
x22
⟶
∀ x31 .
x31
∈
x22
⟶
x18
x20
x23
x24
x25
x26
x27
x28
x29
x30
x31
⟶
5bab1..
x19
x20
)
⟶
∀ x19 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x20 .
∀ x21 :
ι →
ι → ο
.
(
∀ x22 .
x22
∈
x20
⟶
∀ x23 .
x23
∈
x20
⟶
x21
x22
x23
⟶
x21
x23
x22
)
⟶
4402e..
x20
x21
⟶
cf2df..
x20
x21
⟶
∀ x22 .
x22
∈
x20
⟶
∀ x23 .
x23
⊆
setminus
x20
(
Sing
x22
)
⟶
∀ x24 .
x24
∈
x23
⟶
∀ x25 .
x25
∈
x23
⟶
∀ x26 .
x26
∈
x23
⟶
∀ x27 .
x27
∈
x23
⟶
∀ x28 .
x28
∈
x23
⟶
∀ x29 .
x29
∈
x23
⟶
∀ x30 .
x30
∈
x23
⟶
∀ x31 .
x31
∈
x23
⟶
∀ x32 .
x32
∈
x23
⟶
x19
x21
x24
x25
x26
x27
x28
x29
x30
x31
x32
⟶
5bab1..
x20
x21
)
⟶
∀ x20 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x21 .
∀ x22 :
ι →
ι → ο
.
(
∀ x23 .
x23
∈
x21
⟶
∀ x24 .
x24
∈
x21
⟶
x22
x23
x24
⟶
x22
x24
x23
)
⟶
4402e..
x21
x22
⟶
cf2df..
x21
x22
⟶
∀ x23 .
x23
∈
x21
⟶
∀ x24 .
x24
⊆
setminus
x21
(
Sing
x23
)
⟶
∀ x25 .
x25
∈
x24
⟶
∀ x26 .
x26
∈
x24
⟶
∀ x27 .
x27
∈
x24
⟶
∀ x28 .
x28
∈
x24
⟶
∀ x29 .
x29
∈
x24
⟶
∀ x30 .
x30
∈
x24
⟶
∀ x31 .
x31
∈
x24
⟶
∀ x32 .
x32
∈
x24
⟶
∀ x33 .
x33
∈
x24
⟶
x20
x22
x25
x26
x27
x28
x29
x30
x31
x32
x33
⟶
5bab1..
x21
x22
)
⟶
∀ x21 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x22 .
∀ x23 :
ι →
ι → ο
.
(
∀ x24 .
x24
∈
x22
⟶
∀ x25 .
x25
∈
x22
⟶
x23
x24
x25
⟶
x23
x25
x24
)
⟶
4402e..
x22
x23
⟶
cf2df..
x22
x23
⟶
∀ x24 .
x24
∈
x22
⟶
∀ x25 .
x25
⊆
setminus
x22
(
Sing
x24
)
⟶
∀ x26 .
x26
∈
x25
⟶
∀ x27 .
x27
∈
x25
⟶
∀ x28 .
x28
∈
x25
⟶
∀ x29 .
x29
∈
x25
⟶
∀ x30 .
x30
∈
x25
⟶
∀ x31 .
x31
∈
x25
⟶
∀ x32 .
x32
∈
x25
⟶
∀ x33 .
x33
∈
x25
⟶
∀ x34 .
x34
∈
x25
⟶
x21
x23
x26
x27
x28
x29
x30
x31
x32
x33
x34
⟶
5bab1..
x22
x23
)
⟶
∀ x22 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x23 .
∀ x24 :
ι →
ι → ο
.
(
∀ x25 .
x25
∈
x23
⟶
∀ x26 .
x26
∈
x23
⟶
x24
x25
x26
⟶
x24
x26
x25
)
⟶
4402e..
x23
x24
⟶
cf2df..
x23
x24
⟶
∀ x25 .
x25
∈
x23
⟶
∀ x26 .
x26
⊆
setminus
x23
(
Sing
x25
)
⟶
∀ x27 .
x27
∈
x26
⟶
∀ x28 .
x28
∈
x26
⟶
∀ x29 .
x29
∈
x26
⟶
∀ x30 .
x30
∈
x26
⟶
∀ x31 .
x31
∈
x26
⟶
∀ x32 .
x32
∈
x26
⟶
∀ x33 .
x33
∈
x26
⟶
∀ x34 .
x34
∈
x26
⟶
∀ x35 .
x35
∈
x26
⟶
x22
x24
x27
x28
x29
x30
x31
x32
x33
x34
x35
⟶
5bab1..
x23
x24
)
⟶
∀ x23 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x24 .
∀ x25 :
ι →
ι → ο
.
(
∀ x26 .
x26
∈
x24
⟶
∀ x27 .
x27
∈
x24
⟶
x25
x26
x27
⟶
x25
x27
x26
)
⟶
4402e..
x24
x25
⟶
cf2df..
x24
x25
⟶
∀ x26 .
x26
∈
x24
⟶
∀ x27 .
x27
⊆
setminus
x24
(
Sing
x26
)
⟶
∀ x28 .
x28
∈
x27
⟶
∀ x29 .
x29
∈
x27
⟶
∀ x30 .
x30
∈
x27
⟶
∀ x31 .
x31
∈
x27
⟶
∀ x32 .
x32
∈
x27
⟶
∀ x33 .
x33
∈
x27
⟶
∀ x34 .
x34
∈
x27
⟶
∀ x35 .
x35
∈
x27
⟶
∀ x36 .
x36
∈
x27
⟶
x23
x25
x28
x29
x30
x31
x32
x33
x34
x35
x36
⟶
5bab1..
x24
x25
)
⟶
∀ x24 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x25 .
∀ x26 :
ι →
ι → ο
.
(
∀ x27 .
x27
∈
x25
⟶
∀ x28 .
x28
∈
x25
⟶
x26
x27
x28
⟶
x26
x28
x27
)
⟶
4402e..
x25
x26
⟶
cf2df..
x25
x26
⟶
∀ x27 .
x27
∈
x25
⟶
∀ x28 .
x28
⊆
setminus
x25
(
Sing
x27
)
⟶
∀ x29 .
x29
∈
x28
⟶
∀ x30 .
x30
∈
x28
⟶
∀ x31 .
x31
∈
x28
⟶
∀ x32 .
x32
∈
x28
⟶
∀ x33 .
x33
∈
x28
⟶
∀ x34 .
x34
∈
x28
⟶
∀ x35 .
x35
∈
x28
⟶
∀ x36 .
x36
∈
x28
⟶
∀ x37 .
x37
∈
x28
⟶
x24
x26
x29
x30
x31
x32
x33
x34
x35
x36
x37
⟶
5bab1..
x25
x26
)
⟶
∀ x25 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x26 .
∀ x27 :
ι →
ι → ο
.
(
∀ x28 .
x28
∈
x26
⟶
∀ x29 .
x29
∈
x26
⟶
x27
x28
x29
⟶
x27
x29
x28
)
⟶
4402e..
x26
x27
⟶
cf2df..
x26
x27
⟶
∀ x28 .
x28
∈
x26
⟶
∀ x29 .
x29
⊆
setminus
x26
(
Sing
x28
)
⟶
∀ x30 .
x30
∈
x29
⟶
∀ x31 .
x31
∈
x29
⟶
∀ x32 .
x32
∈
x29
⟶
∀ x33 .
x33
∈
x29
⟶
∀ x34 .
x34
∈
x29
⟶
∀ x35 .
x35
∈
x29
⟶
∀ x36 .
x36
∈
x29
⟶
∀ x37 .
x37
∈
x29
⟶
∀ x38 .
x38
∈
x29
⟶
x25
x27
x30
x31
x32
x33
x34
x35
x36
x37
x38
⟶
5bab1..
x26
x27
)
⟶
∀ x26 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x27 .
∀ x28 :
ι →
ι → ο
.
(
∀ x29 .
x29
∈
x27
⟶
∀ x30 .
x30
∈
x27
⟶
x28
x29
x30
⟶
x28
x30
x29
)
⟶
4402e..
x27
x28
⟶
cf2df..
x27
x28
⟶
∀ x29 .
x29
∈
x27
⟶
∀ x30 .
x30
⊆
setminus
x27
(
Sing
x29
)
⟶
∀ x31 .
x31
∈
x30
⟶
∀ x32 .
x32
∈
x30
⟶
∀ x33 .
x33
∈
x30
⟶
∀ x34 .
x34
∈
x30
⟶
∀ x35 .
x35
∈
x30
⟶
∀ x36 .
x36
∈
x30
⟶
∀ x37 .
x37
∈
x30
⟶
∀ x38 .
x38
∈
x30
⟶
∀ x39 .
x39
∈
x30
⟶
x26
x28
x31
x32
x33
x34
x35
x36
x37
x38
x39
⟶
5bab1..
x27
x28
)
⟶
∀ x27 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x28 .
∀ x29 :
ι →
ι → ο
.
(
∀ x30 .
x30
∈
x28
⟶
∀ x31 .
x31
∈
x28
⟶
x29
x30
x31
⟶
x29
x31
x30
)
⟶
4402e..
x28
x29
⟶
cf2df..
x28
x29
⟶
∀ x30 .
x30
∈
x28
⟶
∀ x31 .
x31
⊆
setminus
x28
(
Sing
x30
)
⟶
∀ x32 .
x32
∈
x31
⟶
∀ x33 .
x33
∈
x31
⟶
∀ x34 .
x34
∈
x31
⟶
∀ x35 .
x35
∈
x31
⟶
∀ x36 .
x36
∈
x31
⟶
∀ x37 .
x37
∈
x31
⟶
∀ x38 .
x38
∈
x31
⟶
∀ x39 .
x39
∈
x31
⟶
∀ x40 .
x40
∈
x31
⟶
x27
x29
x32
x33
x34
x35
x36
x37
x38
x39
x40
⟶
5bab1..
x28
x29
)
⟶
∀ x28 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x29 .
∀ x30 :
ι →
ι → ο
.
(
∀ x31 .
x31
∈
x29
⟶
∀ x32 .
x32
∈
x29
⟶
x30
x31
x32
⟶
x30
x32
x31
)
⟶
4402e..
x29
x30
⟶
cf2df..
x29
x30
⟶
∀ x31 .
x31
∈
x29
⟶
∀ x32 .
x32
⊆
setminus
x29
(
Sing
x31
)
⟶
∀ x33 .
x33
∈
x32
⟶
∀ x34 .
x34
∈
x32
⟶
∀ x35 .
x35
∈
x32
⟶
∀ x36 .
x36
∈
x32
⟶
∀ x37 .
x37
∈
x32
⟶
∀ x38 .
x38
∈
x32
⟶
∀ x39 .
x39
∈
x32
⟶
∀ x40 .
x40
∈
x32
⟶
∀ x41 .
x41
∈
x32
⟶
x28
x30
x33
x34
x35
x36
x37
x38
x39
x40
x41
⟶
5bab1..
x29
x30
)
⟶
∀ x29 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x30 .
∀ x31 :
ι →
ι → ο
.
(
∀ x32 .
x32
∈
x30
⟶
∀ x33 .
x33
∈
x30
⟶
x31
x32
x33
⟶
x31
x33
x32
)
⟶
4402e..
x30
x31
⟶
cf2df..
x30
x31
⟶
∀ x32 .
x32
∈
x30
⟶
∀ x33 .
x33
⊆
setminus
x30
(
Sing
x32
)
⟶
∀ x34 .
x34
∈
x33
⟶
∀ x35 .
x35
∈
x33
⟶
∀ x36 .
x36
∈
x33
⟶
∀ x37 .
x37
∈
x33
⟶
∀ x38 .
x38
∈
x33
⟶
∀ x39 .
x39
∈
x33
⟶
∀ x40 .
x40
∈
x33
⟶
∀ x41 .
x41
∈
x33
⟶
∀ x42 .
x42
∈
x33
⟶
x29
x31
x34
x35
x36
x37
x38
x39
x40
x41
x42
⟶
5bab1..
x30
x31
)
⟶
∀ x30 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x31 .
∀ x32 :
ι →
ι → ο
.
(
∀ x33 .
x33
∈
x31
⟶
∀ x34 .
x34
∈
x31
⟶
x32
x33
x34
⟶
x32
x34
x33
)
⟶
4402e..
x31
x32
⟶
cf2df..
x31
x32
⟶
∀ x33 .
x33
∈
x31
⟶
∀ x34 .
x34
⊆
setminus
x31
(
Sing
x33
)
⟶
∀ x35 .
x35
∈
x34
⟶
∀ x36 .
x36
∈
x34
⟶
∀ x37 .
x37
∈
x34
⟶
∀ x38 .
x38
∈
x34
⟶
∀ x39 .
x39
∈
x34
⟶
∀ x40 .
x40
∈
x34
⟶
∀ x41 .
x41
∈
x34
⟶
∀ x42 .
x42
∈
x34
⟶
∀ x43 .
x43
∈
x34
⟶
x30
x32
x35
x36
x37
x38
x39
x40
x41
x42
x43
⟶
5bab1..
x31
x32
)
⟶
∀ x31 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x32 .
∀ x33 :
ι →
ι → ο
.
(
∀ x34 .
x34
∈
x32
⟶
∀ x35 .
x35
∈
x32
⟶
x33
x34
x35
⟶
x33
x35
x34
)
⟶
4402e..
x32
x33
⟶
cf2df..
x32
x33
⟶
∀ x34 .
x34
∈
x32
⟶
∀ x35 .
x35
⊆
setminus
x32
(
Sing
x34
)
⟶
∀ x36 .
x36
∈
x35
⟶
∀ x37 .
x37
∈
x35
⟶
∀ x38 .
x38
∈
x35
⟶
∀ x39 .
x39
∈
x35
⟶
∀ x40 .
x40
∈
x35
⟶
∀ x41 .
x41
∈
x35
⟶
∀ x42 .
x42
∈
x35
⟶
∀ x43 .
x43
∈
x35
⟶
∀ x44 .
x44
∈
x35
⟶
x31
x33
x36
x37
x38
x39
x40
x41
x42
x43
x44
⟶
5bab1..
x32
x33
)
⟶
∀ x32 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x33 .
∀ x34 :
ι →
ι → ο
.
(
∀ x35 .
x35
∈
x33
⟶
∀ x36 .
x36
∈
x33
⟶
x34
x35
x36
⟶
x34
x36
x35
)
⟶
4402e..
x33
x34
⟶
cf2df..
x33
x34
⟶
∀ x35 .
x35
∈
x33
⟶
∀ x36 .
x36
⊆
setminus
x33
(
Sing
x35
)
⟶
∀ x37 .
x37
∈
x36
⟶
∀ x38 .
x38
∈
x36
⟶
∀ x39 .
x39
∈
x36
⟶
∀ x40 .
x40
∈
x36
⟶
∀ x41 .
x41
∈
x36
⟶
∀ x42 .
x42
∈
x36
⟶
∀ x43 .
x43
∈
x36
⟶
∀ x44 .
x44
∈
x36
⟶
∀ x45 .
x45
∈
x36
⟶
x32
x34
x37
x38
x39
x40
x41
x42
x43
x44
x45
⟶
5bab1..
x33
x34
)
⟶
∀ x33 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x34 .
∀ x35 :
ι →
ι → ο
.
(
∀ x36 .
x36
∈
x34
⟶
∀ x37 .
x37
∈
x34
⟶
x35
x36
x37
⟶
x35
x37
x36
)
⟶
4402e..
x34
x35
⟶
cf2df..
x34
x35
⟶
∀ x36 .
x36
∈
x34
⟶
∀ x37 .
x37
⊆
setminus
x34
(
Sing
x36
)
⟶
∀ x38 .
x38
∈
x37
⟶
∀ x39 .
x39
∈
x37
⟶
∀ x40 .
x40
∈
x37
⟶
∀ x41 .
x41
∈
x37
⟶
∀ x42 .
x42
∈
x37
⟶
∀ x43 .
x43
∈
x37
⟶
∀ x44 .
x44
∈
x37
⟶
∀ x45 .
x45
∈
x37
⟶
∀ x46 .
x46
∈
x37
⟶
x33
x35
x38
x39
x40
x41
x42
x43
x44
x45
x46
⟶
5bab1..
x34
x35
)
⟶
∀ x34 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x35 .
∀ x36 :
ι →
ι → ο
.
(
∀ x37 .
x37
∈
x35
⟶
∀ x38 .
x38
∈
x35
⟶
x36
x37
x38
⟶
x36
x38
x37
)
⟶
4402e..
x35
x36
⟶
cf2df..
x35
x36
⟶
∀ x37 .
x37
∈
x35
⟶
∀ x38 .
x38
⊆
setminus
x35
(
Sing
x37
)
⟶
∀ x39 .
x39
∈
x38
⟶
∀ x40 .
x40
∈
x38
⟶
∀ x41 .
x41
∈
x38
⟶
∀ x42 .
x42
∈
x38
⟶
∀ x43 .
x43
∈
x38
⟶
∀ x44 .
x44
∈
x38
⟶
∀ x45 .
x45
∈
x38
⟶
∀ x46 .
x46
∈
x38
⟶
∀ x47 .
x47
∈
x38
⟶
x34
x36
x39
x40
x41
x42
x43
x44
x45
x46
x47
⟶
5bab1..
x35
x36
)
⟶
∀ x35 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x36 .
∀ x37 :
ι →
ι → ο
.
(
∀ x38 .
x38
∈
x36
⟶
∀ x39 .
x39
∈
x36
⟶
x37
x38
x39
⟶
x37
x39
x38
)
⟶
4402e..
x36
x37
⟶
cf2df..
x36
x37
⟶
∀ x38 .
x38
∈
x36
⟶
∀ x39 .
x39
⊆
setminus
x36
(
Sing
x38
)
⟶
∀ x40 .
x40
∈
x39
⟶
∀ x41 .
x41
∈
x39
⟶
∀ x42 .
x42
∈
x39
⟶
∀ x43 .
x43
∈
x39
⟶
∀ x44 .
x44
∈
x39
⟶
∀ x45 .
x45
∈
x39
⟶
∀ x46 .
x46
∈
x39
⟶
∀ x47 .
x47
∈
x39
⟶
∀ x48 .
x48
∈
x39
⟶
x35
x37
x40
x41
x42
x43
x44
x45
x46
x47
x48
⟶
5bab1..
x36
x37
)
⟶
∀ x36 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x37 .
∀ x38 :
ι →
ι → ο
.
(
∀ x39 .
x39
∈
x37
⟶
∀ x40 .
x40
∈
x37
⟶
x38
x39
x40
⟶
x38
x40
x39
)
⟶
4402e..
x37
x38
⟶
cf2df..
x37
x38
⟶
∀ x39 .
x39
∈
x37
⟶
∀ x40 .
x40
⊆
setminus
x37
(
Sing
x39
)
⟶
∀ x41 .
x41
∈
x40
⟶
∀ x42 .
x42
∈
x40
⟶
∀ x43 .
x43
∈
x40
⟶
∀ x44 .
x44
∈
x40
⟶
∀ x45 .
x45
∈
x40
⟶
∀ x46 .
x46
∈
x40
⟶
∀ x47 .
x47
∈
x40
⟶
∀ x48 .
x48
∈
x40
⟶
∀ x49 .
x49
∈
x40
⟶
x36
x38
x41
x42
x43
x44
x45
x46
x47
x48
x49
⟶
5bab1..
x37
x38
)
⟶
∀ x37 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x38 .
∀ x39 :
ι →
ι → ο
.
(
∀ x40 .
x40
∈
x38
⟶
∀ x41 .
x41
∈
x38
⟶
x39
x40
x41
⟶
x39
x41
x40
)
⟶
4402e..
x38
x39
⟶
cf2df..
x38
x39
⟶
∀ x40 .
x40
∈
x38
⟶
∀ x41 .
x41
⊆
setminus
x38
(
Sing
x40
)
⟶
∀ x42 .
x42
∈
x41
⟶
∀ x43 .
x43
∈
x41
⟶
∀ x44 .
x44
∈
x41
⟶
∀ x45 .
x45
∈
x41
⟶
∀ x46 .
x46
∈
x41
⟶
∀ x47 .
x47
∈
x41
⟶
∀ x48 .
x48
∈
x41
⟶
∀ x49 .
x49
∈
x41
⟶
∀ x50 .
x50
∈
x41
⟶
x37
x39
x42
x43
x44
x45
x46
x47
x48
x49
x50
⟶
5bab1..
x38
x39
)
⟶
∀ x38 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x39 .
∀ x40 :
ι →
ι → ο
.
(
∀ x41 .
x41
∈
x39
⟶
∀ x42 .
x42
∈
x39
⟶
x40
x41
x42
⟶
x40
x42
x41
)
⟶
4402e..
x39
x40
⟶
cf2df..
x39
x40
⟶
∀ x41 .
x41
∈
x39
⟶
∀ x42 .
x42
⊆
setminus
x39
(
Sing
x41
)
⟶
∀ x43 .
x43
∈
x42
⟶
∀ x44 .
x44
∈
x42
⟶
∀ x45 .
x45
∈
x42
⟶
∀ x46 .
x46
∈
x42
⟶
∀ x47 .
x47
∈
x42
⟶
∀ x48 .
x48
∈
x42
⟶
∀ x49 .
x49
∈
x42
⟶
∀ x50 .
x50
∈
x42
⟶
∀ x51 .
x51
∈
x42
⟶
x38
x40
x43
x44
x45
x46
x47
x48
x49
x50
x51
⟶
5bab1..
x39
x40
)
⟶
∀ x39 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x40 .
∀ x41 :
ι →
ι → ο
.
(
∀ x42 .
x42
∈
x40
⟶
∀ x43 .
x43
∈
x40
⟶
x41
x42
x43
⟶
x41
x43
x42
)
⟶
4402e..
x40
x41
⟶
cf2df..
x40
x41
⟶
∀ x42 .
x42
∈
x40
⟶
∀ x43 .
x43
⊆
setminus
x40
(
Sing
x42
)
⟶
∀ x44 .
x44
∈
x43
⟶
∀ x45 .
x45
∈
x43
⟶
∀ x46 .
x46
∈
x43
⟶
∀ x47 .
x47
∈
x43
⟶
∀ x48 .
x48
∈
x43
⟶
∀ x49 .
x49
∈
x43
⟶
∀ x50 .
x50
∈
x43
⟶
∀ x51 .
x51
∈
x43
⟶
∀ x52 .
x52
∈
x43
⟶
x39
x41
x44
x45
x46
x47
x48
x49
x50
x51
x52
⟶
5bab1..
x40
x41
)
⟶
∀ x40 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x41 .
∀ x42 :
ι →
ι → ο
.
(
∀ x43 .
x43
∈
x41
⟶
∀ x44 .
x44
∈
x41
⟶
x42
x43
x44
⟶
x42
x44
x43
)
⟶
4402e..
x41
x42
⟶
cf2df..
x41
x42
⟶
∀ x43 .
x43
∈
x41
⟶
∀ x44 .
x44
⊆
setminus
x41
(
Sing
x43
)
⟶
∀ x45 .
x45
∈
x44
⟶
∀ x46 .
x46
∈
x44
⟶
∀ x47 .
x47
∈
x44
⟶
∀ x48 .
x48
∈
x44
⟶
∀ x49 .
x49
∈
x44
⟶
∀ x50 .
x50
∈
x44
⟶
∀ x51 .
x51
∈
x44
⟶
∀ x52 .
x52
∈
x44
⟶
∀ x53 .
x53
∈
x44
⟶
x40
x42
x45
x46
x47
x48
x49
x50
x51
x52
x53
⟶
5bab1..
x41
x42
)
⟶
∀ x41 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x42 .
∀ x43 :
ι →
ι → ο
.
(
∀ x44 .
x44
∈
x42
⟶
∀ x45 .
x45
∈
x42
⟶
x43
x44
x45
⟶
x43
x45
x44
)
⟶
4402e..
x42
x43
⟶
cf2df..
x42
x43
⟶
∀ x44 .
x44
∈
x42
⟶
∀ x45 .
x45
⊆
setminus
x42
(
Sing
x44
)
⟶
∀ x46 .
x46
∈
x45
⟶
∀ x47 .
x47
∈
x45
⟶
∀ x48 .
x48
∈
x45
⟶
∀ x49 .
x49
∈
x45
⟶
∀ x50 .
x50
∈
x45
⟶
∀ x51 .
x51
∈
x45
⟶
∀ x52 .
x52
∈
x45
⟶
∀ x53 .
x53
∈
x45
⟶
∀ x54 .
x54
∈
x45
⟶
x41
x43
x46
x47
x48
x49
x50
x51
x52
x53
x54
⟶
5bab1..
x42
x43
)
⟶
∀ x42 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x43 .
∀ x44 :
ι →
ι → ο
.
(
∀ x45 .
x45
∈
x43
⟶
∀ x46 .
x46
∈
x43
⟶
x44
x45
x46
⟶
x44
x46
x45
)
⟶
4402e..
x43
x44
⟶
cf2df..
x43
x44
⟶
∀ x45 .
x45
∈
x43
⟶
∀ x46 .
x46
⊆
setminus
x43
(
Sing
x45
)
⟶
∀ x47 .
x47
∈
x46
⟶
∀ x48 .
x48
∈
x46
⟶
∀ x49 .
x49
∈
x46
⟶
∀ x50 .
x50
∈
x46
⟶
∀ x51 .
x51
∈
x46
⟶
∀ x52 .
x52
∈
x46
⟶
∀ x53 .
x53
∈
x46
⟶
∀ x54 .
x54
∈
x46
⟶
∀ x55 .
x55
∈
x46
⟶
x42
x44
x47
x48
x49
x50
x51
x52
x53
x54
x55
⟶
5bab1..
x43
x44
)
⟶
∀ x43 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x44 .
∀ x45 :
ι →
ι → ο
.
(
∀ x46 .
x46
∈
x44
⟶
∀ x47 .
x47
∈
x44
⟶
x45
x46
x47
⟶
x45
x47
x46
)
⟶
4402e..
x44
x45
⟶
cf2df..
x44
x45
⟶
∀ x46 .
x46
∈
x44
⟶
∀ x47 .
x47
⊆
setminus
x44
(
Sing
x46
)
⟶
∀ x48 .
x48
∈
x47
⟶
∀ x49 .
x49
∈
x47
⟶
∀ x50 .
x50
∈
x47
⟶
∀ x51 .
x51
∈
x47
⟶
∀ x52 .
x52
∈
x47
⟶
∀ x53 .
x53
∈
x47
⟶
∀ x54 .
x54
∈
x47
⟶
∀ x55 .
x55
∈
x47
⟶
∀ x56 .
x56
∈
x47
⟶
x43
x45
x48
x49
x50
x51
x52
x53
x54
x55
x56
⟶
5bab1..
x44
x45
)
⟶
∀ x44 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x45 .
∀ x46 :
ι →
ι → ο
.
(
∀ x47 .
x47
∈
x45
⟶
∀ x48 .
x48
∈
x45
⟶
x46
x47
x48
⟶
x46
x48
x47
)
⟶
4402e..
x45
x46
⟶
cf2df..
x45
x46
⟶
∀ x47 .
x47
∈
x45
⟶
∀ x48 .
x48
⊆
setminus
x45
(
Sing
x47
)
⟶
∀ x49 .
x49
∈
x48
⟶
∀ x50 .
x50
∈
x48
⟶
∀ x51 .
x51
∈
x48
⟶
∀ x52 .
x52
∈
x48
⟶
∀ x53 .
x53
∈
x48
⟶
∀ x54 .
x54
∈
x48
⟶
∀ x55 .
x55
∈
x48
⟶
∀ x56 .
x56
∈
x48
⟶
∀ x57 .
x57
∈
x48
⟶
x44
x46
x49
x50
x51
x52
x53
x54
x55
x56
x57
⟶
5bab1..
x45
x46
)
⟶
∀ x45 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x46 .
∀ x47 :
ι →
ι → ο
.
(
∀ x48 .
x48
∈
x46
⟶
∀ x49 .
x49
∈
x46
⟶
x47
x48
x49
⟶
x47
x49
x48
)
⟶
4402e..
x46
x47
⟶
cf2df..
x46
x47
⟶
∀ x48 .
x48
∈
x46
⟶
∀ x49 .
x49
⊆
setminus
x46
(
Sing
x48
)
⟶
∀ x50 .
x50
∈
x49
⟶
∀ x51 .
x51
∈
x49
⟶
∀ x52 .
x52
∈
x49
⟶
∀ x53 .
x53
∈
x49
⟶
∀ x54 .
x54
∈
x49
⟶
∀ x55 .
x55
∈
x49
⟶
∀ x56 .
x56
∈
x49
⟶
∀ x57 .
x57
∈
x49
⟶
∀ x58 .
x58
∈
x49
⟶
x45
x47
x50
x51
x52
x53
x54
x55
x56
x57
x58
⟶
5bab1..
x46
x47
)
⟶
∀ x46 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x47 .
∀ x48 :
ι →
ι → ο
.
(
∀ x49 .
x49
∈
x47
⟶
∀ x50 .
x50
∈
x47
⟶
x48
x49
x50
⟶
x48
x50
x49
)
⟶
4402e..
x47
x48
⟶
cf2df..
x47
x48
⟶
∀ x49 .
x49
∈
x47
⟶
∀ x50 .
x50
⊆
setminus
x47
(
Sing
x49
)
⟶
∀ x51 .
x51
∈
x50
⟶
∀ x52 .
x52
∈
x50
⟶
∀ x53 .
x53
∈
x50
⟶
∀ x54 .
x54
∈
x50
⟶
∀ x55 .
x55
∈
x50
⟶
∀ x56 .
x56
∈
x50
⟶
∀ x57 .
x57
∈
x50
⟶
∀ x58 .
x58
∈
x50
⟶
∀ x59 .
x59
∈
x50
⟶
x46
x48
x51
x52
x53
x54
x55
x56
x57
x58
x59
⟶
5bab1..
x47
x48
)
⟶
∀ x47 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x48 .
∀ x49 :
ι →
ι → ο
.
(
∀ x50 .
x50
∈
x48
⟶
∀ x51 .
x51
∈
x48
⟶
x49
x50
x51
⟶
x49
x51
x50
)
⟶
4402e..
x48
x49
⟶
cf2df..
x48
x49
⟶
∀ x50 .
x50
∈
x48
⟶
∀ x51 .
x51
⊆
setminus
x48
(
Sing
x50
)
⟶
∀ x52 .
x52
∈
x51
⟶
∀ x53 .
x53
∈
x51
⟶
∀ x54 .
x54
∈
x51
⟶
∀ x55 .
x55
∈
x51
⟶
∀ x56 .
x56
∈
x51
⟶
∀ x57 .
x57
∈
x51
⟶
∀ x58 .
x58
∈
x51
⟶
∀ x59 .
x59
∈
x51
⟶
∀ x60 .
x60
∈
x51
⟶
x47
x49
x52
x53
x54
x55
x56
x57
x58
x59
x60
⟶
5bab1..
x48
x49
)
⟶
∀ x48 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x49 .
∀ x50 :
ι →
ι → ο
.
(
∀ x51 .
x51
∈
x49
⟶
∀ x52 .
x52
∈
x49
⟶
x50
x51
x52
⟶
x50
x52
x51
)
⟶
4402e..
x49
x50
⟶
cf2df..
x49
x50
⟶
∀ x51 .
x51
∈
x49
⟶
∀ x52 .
x52
⊆
setminus
x49
(
Sing
x51
)
⟶
∀ x53 .
x53
∈
x52
⟶
∀ x54 .
x54
∈
x52
⟶
∀ x55 .
x55
∈
x52
⟶
∀ x56 .
x56
∈
x52
⟶
∀ x57 .
x57
∈
x52
⟶
∀ x58 .
x58
∈
x52
⟶
∀ x59 .
x59
∈
x52
⟶
∀ x60 .
x60
∈
x52
⟶
∀ x61 .
x61
∈
x52
⟶
x48
x50
x53
x54
x55
x56
x57
x58
x59
x60
x61
⟶
5bab1..
x49
x50
)
⟶
∀ x49 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x50 .
∀ x51 :
ι →
ι → ο
.
(
∀ x52 .
x52
∈
x50
⟶
∀ x53 .
x53
∈
x50
⟶
x51
x52
x53
⟶
x51
x53
x52
)
⟶
4402e..
x50
x51
⟶
cf2df..
x50
x51
⟶
∀ x52 .
x52
∈
x50
⟶
∀ x53 .
x53
⊆
setminus
x50
(
Sing
x52
)
⟶
∀ x54 .
x54
∈
x53
⟶
∀ x55 .
x55
∈
x53
⟶
∀ x56 .
x56
∈
x53
⟶
∀ x57 .
x57
∈
x53
⟶
∀ x58 .
x58
∈
x53
⟶
∀ x59 .
x59
∈
x53
⟶
∀ x60 .
x60
∈
x53
⟶
∀ x61 .
x61
∈
x53
⟶
∀ x62 .
x62
∈
x53
⟶
x49
x51
x54
x55
x56
x57
x58
x59
x60
x61
x62
⟶
5bab1..
x50
x51
)
⟶
∀ x50 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x51 .
∀ x52 :
ι →
ι → ο
.
(
∀ x53 .
x53
∈
x51
⟶
∀ x54 .
x54
∈
x51
⟶
x52
x53
x54
⟶
x52
x54
x53
)
⟶
4402e..
x51
x52
⟶
cf2df..
x51
x52
⟶
∀ x53 .
x53
∈
x51
⟶
∀ x54 .
x54
⊆
setminus
x51
(
Sing
x53
)
⟶
∀ x55 .
x55
∈
x54
⟶
∀ x56 .
x56
∈
x54
⟶
∀ x57 .
x57
∈
x54
⟶
∀ x58 .
x58
∈
x54
⟶
∀ x59 .
x59
∈
x54
⟶
∀ x60 .
x60
∈
x54
⟶
∀ x61 .
x61
∈
x54
⟶
∀ x62 .
x62
∈
x54
⟶
∀ x63 .
x63
∈
x54
⟶
x50
x52
x55
x56
x57
x58
x59
x60
x61
x62
x63
⟶
5bab1..
x51
x52
)
⟶
∀ x51 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x52 .
∀ x53 :
ι →
ι → ο
.
(
∀ x54 .
x54
∈
x52
⟶
∀ x55 .
x55
∈
x52
⟶
x53
x54
x55
⟶
x53
x55
x54
)
⟶
4402e..
x52
x53
⟶
cf2df..
x52
x53
⟶
∀ x54 .
x54
∈
x52
⟶
∀ x55 .
x55
⊆
setminus
x52
(
Sing
x54
)
⟶
∀ x56 .
x56
∈
x55
⟶
∀ x57 .
x57
∈
x55
⟶
∀ x58 .
x58
∈
x55
⟶
∀ x59 .
x59
∈
x55
⟶
∀ x60 .
x60
∈
x55
⟶
∀ x61 .
x61
∈
x55
⟶
∀ x62 .
x62
∈
x55
⟶
∀ x63 .
x63
∈
x55
⟶
∀ x64 .
x64
∈
x55
⟶
x51
x53
x56
x57
x58
x59
x60
x61
x62
x63
x64
⟶
5bab1..
x52
x53
)
⟶
∀ x52 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x53 .
∀ x54 :
ι →
ι → ο
.
(
∀ x55 .
x55
∈
x53
⟶
∀ x56 .
x56
∈
x53
⟶
x54
x55
x56
⟶
x54
x56
x55
)
⟶
4402e..
x53
x54
⟶
cf2df..
x53
x54
⟶
∀ x55 .
x55
∈
x53
⟶
∀ x56 .
x56
⊆
setminus
x53
(
Sing
x55
)
⟶
∀ x57 .
x57
∈
x56
⟶
∀ x58 .
x58
∈
x56
⟶
∀ x59 .
x59
∈
x56
⟶
∀ x60 .
x60
∈
x56
⟶
∀ x61 .
x61
∈
x56
⟶
∀ x62 .
x62
∈
x56
⟶
∀ x63 .
x63
∈
x56
⟶
∀ x64 .
x64
∈
x56
⟶
∀ x65 .
x65
∈
x56
⟶
x52
x54
x57
x58
x59
x60
x61
x62
x63
x64
x65
⟶
5bab1..
x53
x54
)
⟶
∀ x53 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x54 .
∀ x55 :
ι →
ι → ο
.
(
∀ x56 .
x56
∈
x54
⟶
∀ x57 .
x57
∈
x54
⟶
x55
x56
x57
⟶
x55
x57
x56
)
⟶
4402e..
x54
x55
⟶
cf2df..
x54
x55
⟶
∀ x56 .
x56
∈
x54
⟶
∀ x57 .
x57
⊆
setminus
x54
(
Sing
x56
)
⟶
∀ x58 .
x58
∈
x57
⟶
∀ x59 .
x59
∈
x57
⟶
∀ x60 .
x60
∈
x57
⟶
∀ x61 .
x61
∈
x57
⟶
∀ x62 .
x62
∈
x57
⟶
∀ x63 .
x63
∈
x57
⟶
∀ x64 .
x64
∈
x57
⟶
∀ x65 .
x65
∈
x57
⟶
∀ x66 .
x66
∈
x57
⟶
x53
x55
x58
x59
x60
x61
x62
x63
x64
x65
x66
⟶
5bab1..
x54
x55
)
⟶
∀ x54 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x55 .
∀ x56 :
ι →
ι → ο
.
(
∀ x57 .
x57
∈
x55
⟶
∀ x58 .
x58
∈
x55
⟶
x56
x57
x58
⟶
x56
x58
x57
)
⟶
4402e..
x55
x56
⟶
cf2df..
x55
x56
⟶
∀ x57 .
x57
∈
x55
⟶
∀ x58 .
x58
⊆
setminus
x55
(
Sing
x57
)
⟶
∀ x59 .
x59
∈
x58
⟶
∀ x60 .
x60
∈
x58
⟶
∀ x61 .
x61
∈
x58
⟶
∀ x62 .
x62
∈
x58
⟶
∀ x63 .
x63
∈
x58
⟶
∀ x64 .
x64
∈
x58
⟶
∀ x65 .
x65
∈
x58
⟶
∀ x66 .
x66
∈
x58
⟶
∀ x67 .
x67
∈
x58
⟶
x54
x56
x59
x60
x61
x62
x63
x64
x65
x66
x67
⟶
5bab1..
x55
x56
)
⟶
∀ x55 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x56 .
∀ x57 :
ι →
ι → ο
.
(
∀ x58 .
x58
∈
x56
⟶
∀ x59 .
x59
∈
x56
⟶
x57
x58
x59
⟶
x57
x59
x58
)
⟶
4402e..
x56
x57
⟶
cf2df..
x56
x57
⟶
∀ x58 .
x58
∈
x56
⟶
∀ x59 .
x59
⊆
setminus
x56
(
Sing
x58
)
⟶
∀ x60 .
x60
∈
x59
⟶
∀ x61 .
x61
∈
x59
⟶
∀ x62 .
x62
∈
x59
⟶
∀ x63 .
x63
∈
x59
⟶
∀ x64 .
x64
∈
x59
⟶
∀ x65 .
x65
∈
x59
⟶
∀ x66 .
x66
∈
x59
⟶
∀ x67 .
x67
∈
x59
⟶
∀ x68 .
x68
∈
x59
⟶
x55
x57
x60
x61
x62
x63
x64
x65
x66
x67
x68
⟶
5bab1..
x56
x57
)
⟶
∀ x56 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x57 .
∀ x58 :
ι →
ι → ο
.
(
∀ x59 .
x59
∈
x57
⟶
∀ x60 .
x60
∈
x57
⟶
x58
x59
x60
⟶
x58
x60
x59
)
⟶
4402e..
x57
x58
⟶
cf2df..
x57
x58
⟶
∀ x59 .
x59
∈
x57
⟶
∀ x60 .
x60
⊆
setminus
x57
(
Sing
x59
)
⟶
∀ x61 .
x61
∈
x60
⟶
∀ x62 .
x62
∈
x60
⟶
∀ x63 .
x63
∈
x60
⟶
∀ x64 .
x64
∈
x60
⟶
∀ x65 .
x65
∈
x60
⟶
∀ x66 .
x66
∈
x60
⟶
∀ x67 .
x67
∈
x60
⟶
∀ x68 .
x68
∈
x60
⟶
∀ x69 .
x69
∈
x60
⟶
x56
x58
x61
x62
x63
x64
x65
x66
x67
x68
x69
⟶
5bab1..
x57
x58
)
⟶
∀ x57 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x58 .
∀ x59 :
ι →
ι → ο
.
(
∀ x60 .
x60
∈
x58
⟶
∀ x61 .
x61
∈
x58
⟶
x59
x60
x61
⟶
x59
x61
x60
)
⟶
4402e..
x58
x59
⟶
cf2df..
x58
x59
⟶
∀ x60 .
x60
∈
x58
⟶
∀ x61 .
x61
⊆
setminus
x58
(
Sing
x60
)
⟶
∀ x62 .
x62
∈
x61
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
∀ x65 .
x65
∈
x61
⟶
∀ x66 .
x66
∈
x61
⟶
∀ x67 .
x67
∈
x61
⟶
∀ x68 .
x68
∈
x61
⟶
∀ x69 .
x69
∈
x61
⟶
∀ x70 .
x70
∈
x61
⟶
x57
x59
x62
x63
x64
x65
x66
x67
x68
x69
x70
⟶
5bab1..
x58
x59
)
⟶
∀ x58 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x59 .
∀ x60 :
ι →
ι → ο
.
(
∀ x61 .
x61
∈
x59
⟶
∀ x62 .
x62
∈
x59
⟶
x60
x61
x62
⟶
x60
x62
x61
)
⟶
4402e..
x59
x60
⟶
cf2df..
x59
x60
⟶
∀ x61 .
x61
∈
x59
⟶
∀ x62 .
x62
⊆
setminus
x59
(
Sing
x61
)
⟶
∀ x63 .
x63
∈
x62
⟶
∀ x64 .
x64
∈
x62
⟶
∀ x65 .
x65
∈
x62
⟶
∀ x66 .
x66
∈
x62
⟶
∀ x67 .
x67
∈
x62
⟶
∀ x68 .
x68
∈
x62
⟶
∀ x69 .
x69
∈
x62
⟶
∀ x70 .
x70
∈
x62
⟶
∀ x71 .
x71
∈
x62
⟶
x58
x60
x63
x64
x65
x66
x67
x68
x69
x70
x71
⟶
5bab1..
x59
x60
)
⟶
∀ x59 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x60 .
∀ x61 :
ι →
ι → ο
.
(
∀ x62 .
x62
∈
x60
⟶
∀ x63 .
x63
∈
x60
⟶
x61
x62
x63
⟶
x61
x63
x62
)
⟶
4402e..
x60
x61
⟶
cf2df..
x60
x61
⟶
∀ x62 .
x62
∈
x60
⟶
∀ x63 .
x63
⊆
setminus
x60
(
Sing
x62
)
⟶
∀ x64 .
x64
∈
x63
⟶
∀ x65 .
x65
∈
x63
⟶
∀ x66 .
x66
∈
x63
⟶
∀ x67 .
x67
∈
x63
⟶
∀ x68 .
x68
∈
x63
⟶
∀ x69 .
x69
∈
x63
⟶
∀ x70 .
x70
∈
x63
⟶
∀ x71 .
x71
∈
x63
⟶
∀ x72 .
x72
∈
x63
⟶
x59
x61
x64
x65
x66
x67
x68
x69
x70
x71
x72
⟶
5bab1..
x60
x61
)
⟶
∀ x60 :
(
ι →
ι → ο
)
→
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ο
.
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
x60
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
654b9..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
7e5de..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a3794..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
093ca..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
34ae8..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
96162..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
3c407..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
d92ce..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
105be..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a2064..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
f5da9..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b9a4e..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
6e81c..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
4e91d..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
8c9ed..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
37e04..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
13b7c..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
2bf4d..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
53286..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
7db3a..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
22587..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
4d3d7..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
de118..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b0749..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
54c7d..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
cf078..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b43ab..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
96c31..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
627df..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
74622..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
3f98b..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a0d70..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
dbf71..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
f842a..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
23b40..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
d5d69..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
2e1d5..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
94f0c..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
923e2..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
1a9fd..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b39ef..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
0788d..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
e2ec9..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
65996..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
45286..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
8bd80..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
729bd..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
76a6c..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
8d9b1..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
1668d..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
c4d5c..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
e37fb..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
e8ba7..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
7f17b..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
d2e51..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
9eede..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
150dd..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
2c550..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
286f8..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b8d2a..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
05795..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
59a16..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
cec27..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
ba960..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
c2e8a..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
adf05..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
07c0f..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b7a83..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
74a95..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
fc090..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
72d65..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
b7e1a..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
e5024..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
91113..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
f0823..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a9907..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
4b4dd..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a47b6..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
aa358..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
ee649..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
57f60..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
a7e88..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶
59632..
x62
x65
x66
x67
x68
x69
x70
x71
x72
x73
⟶
5bab1..
x61
x62
)
⟶
(
∀ x61 .
∀ x62 :
ι →
ι → ο
.
(
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
∈
x61
⟶
x62
x63
x64
⟶
x62
x64
x63
)
⟶
4402e..
x61
x62
⟶
cf2df..
x61
x62
⟶
∀ x63 .
x63
∈
x61
⟶
∀ x64 .
x64
⊆
setminus
x61
(
Sing
x63
)
⟶
∀ x65 .
x65
∈
x64
⟶
∀ x66 .
x66
∈
x64
⟶
∀ x67 .
x67
∈
x64
⟶
∀ x68 .
x68
∈
x64
⟶
∀ x69 .
x69
∈
x64
⟶
∀ x70 .
x70
∈
x64
⟶
∀ x71 .
x71
∈
x64
⟶
∀ x72 .
x72
∈
x64
⟶
∀ x73 .
x73
∈
x64
⟶