From d9b5ebc7382f64a7e7ecd5d406fb6ffe13d263c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jan 2014 09:18:40 -0800
Subject: [PATCH] refactor(builtin/kernel): cleanup Hilbert operator definition

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean      |  20 ++++++++++----------
 src/builtin/obj/kernel.olean | Bin 25921 -> 26580 bytes
 src/kernel/kernel_decls.cpp  |   4 ++++
 src/kernel/kernel_decls.h    |  17 +++++++++++++++--
 4 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 88de1890b1..6af5c9be7e 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -45,7 +45,8 @@ definition Exists (A : TypeU) (P : A → Bool) := ¬ (∀ x, ¬ (P x))
 
 definition nonempty (A : TypeU) := ∃ x : A, true
 
-theorem nonempty_intro {A : TypeU} (a : A) : (nonempty A)
+-- If we have an element of type A, then A is nonempty
+theorem nonempty_intro {A : TypeU} (a : A) : nonempty A
 := assume H : (∀ x, ¬ true), (H a)
 
 theorem em (a : Bool) : a ∨ ¬ a
@@ -66,11 +67,14 @@ axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x
 -- Epsilon (Hilbert's operator)
 variable eps {A : TypeU} (H : nonempty A) (P : A → Bool) : A
 alias ε : eps
-axiom eps_ax {A : TypeU} {P : A → Bool} {a : A} : P a → P (ε (nonempty_intro a) P)
+axiom eps_ax {A : TypeU} (H : nonempty A) {P : A → Bool} (a : A) : P a → P (ε H P)
 
 -- Proof irrelevance
 axiom proof_irrel {a : Bool} (H1 H2 : a) : H1 = H2
 
+theorem eps_th {A : TypeU} {P : A → Bool} (a : A) : P a → P (ε (nonempty_intro a) P)
+:= assume H : P a, @eps_ax A (nonempty_intro a) P a H
+
 -- Alias for subst where we can provide P explicitly, but keep A,a,b implicit
 theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
 := subst H1 H2
@@ -210,16 +214,12 @@ theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonemp
 := exists_elim H (λ (w : A) (Hw : P w), exists_intro w trivial)
 
 theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P)
-:= exists_elim H (λ (w : A) (Hw : P w),
-                    let Peps : P (ε (nonempty_intro w) P)                 := @eps_ax A P w Hw,
-                        eqpr : (nonempty_intro w) = (nonempty_ex_intro H) := proof_irrel (nonempty_intro w) (nonempty_ex_intro H)
-                        in subst Peps eqpr)
+:= exists_elim H (λ (w : A) (Hw : P w), @eps_ax A (nonempty_ex_intro H) P w Hw)
 
-theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (Hne : nonempty A) (H : ∀ x, ∃ y, R x y) :
-        ∃ f, ∀ x, R x (f x)
+theorem axiom_of_choice {A : TypeU} {B : TypeU} {R : A → B → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
 := exists_intro
-      (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y))  -- witness for f
-      (λ x, exists_to_eps (H x))                       -- proof that witness satisfies ∀ x, R x (f x)
+      (λ x, ε (nonempty_ex_intro (H x)) (λ y, R x y)) -- witness for f
+      (λ x, exists_to_eps (H x))                      -- proof that witness satisfies ∀ x, R x (f x)
 
 theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := or_elim (boolcomplete a)
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 81a63524bf7c3ce1b5f6884a9f124e26c3ee4e69..c927d1ac2e9df35d53a0851ab4207695668c91b4 100644
GIT binary patch
literal 26580
zcmcIt36vdGnXX&!)$52I6eU4JBtXc9MhK#!xIj2M>5L32?TpL-kM2%4Y3U_&Iw24o
zJcb<+kRa;d0tm?nGHx(L7DFIJnS(fpIwH;pI_?hR!X^mwf8TePdetu-!a39D<n~|p
z{`cSi|K6%w)fpY??->~w9O}>fk6Se|xVnFAWq+2xFLTa%t;u^w$FpVq16kgE>WcpN
zWgTIFlRD7mt9!<>eDUb$kd3n2^{yHm8Xp|V-1yk4{w!V%^b8qwQX4U{jl3tTX(Fc;
z1%9c)Sk7K+>VGpj-ZMTpI)V<DZ@HcW^K1B37roIjl0y#(G}!LK>mu*P@2mjP*?@Kd
zY0BE!O8WHEGf>@&q+gV^4jy}e20>xB)}cqv-B=o<hCL(8fSA3wFs}G1q8yR|(%`2P
z&D2(UbLW!WY|8P{iW~<Vt3k}0-a7A*b2pU6D97ONilM>&l|XJMON$hp(N+B?XI;Z9
zvfO^#k8`bT-b&*ggrOO7r{Oj7!^zwH7KnB<yy>Z<{JR%s?Me5{0@y)tZ-AXL%pAZo
z;37r<=XO9E{JhHkRmFMayw6D>n(I}Hh{1sYPH1C)F~BH!i$SY~Z&~;@D)UN`+_&O^
zN6ucaQP5aG3-qrUTsgjyMnLDDjr`ro4Co;%nP5IK*s%cM{?faVufbI?13M*~Y&<&B
zKfGf6)WieGqPP&?p8M5uF9t5nvYsH*v^Ksx%SSwo=HSTq*l3~@9j1tT4d-`K!bO1P
zFFM?)F0qL%q5`ExdC96XIO{;`cMgpEhod!${eZq3nhq&Wkj&ly&=O_Ih;m~whkDjz
zd0&r}4j2_bjYhs?ky2T@+4VuXrork#pJFybsD?Qmpfc7!Fw{otIY5|!M)n32Bkrws
z;T&eKT-Cc0W$SQ^!^ILZMS0oj3~nnqErQOXpkfEf>LApGW)@AsNnOEwhgpB!*$<cx
ztQzTG)53jmG%1Z>@(fsycMNDQY~&|q4M0btDX}n-lM}m=`b&Y=M6*zxX?8aS?8X?`
zQPk+^CDt89?HL-HAS&kV-^h=^?`&q7{j9{kz+jm@uFZzhiFR7ra@7o`dXFL2%u-y7
z`d73h;u1y1As}XoD}-j^YF3zjj9r+ShX#9AX8E^o%#;Sl*z#o3!1_kAX}?RphsIep
z9_fW>Fc&K<7Rsa4jtbCra(3VgU286*gIA1=jt(>j$Hw{*qN1Vr0V8;f`KJ)wJ5cDi
zF`r^4qNQ3%L}_YP7qQL&OpvT=zZ!TTU41w*4`$IHA3&!Hz)1l2XYUZePSgVYESy)%
z5A!x+2h}_qpyC8j%&0-T$R#vWY6V8KV~dbjVa2pk)5{^_BVFEW3|Ww}qYaWh-lvVg
zVO%XJn+zSQ-+GW>U@N(U<-ipoqq;aAOJcG-c~3z*m2^)9sDgVMKn_K%;A8KJ@t(39
zSj4j9ke>KCehykzn-hYJG!l!rmc!G5BAb5@;Bn;tj{uLKM_<YA^3W;hCkez;b|sov
z{AbCxsA3_vf(6!EkNIKvq~_R|#l5XEJ*$SsGZ<uiY;g5p51pLVSg<!@KE>cl($l+g
z)!4F019d89)H&r$P9}I3KxxVNAlBQ0Nb79S8}VdY@k7K~9w-u0Ld=Z`LCs}}a}%HQ
z5_mqqx#WHUz*+OrUW$gD%1MGWB_S3$HnGT^V-w6?m7T)r47_FZ$~o1I!sQ><D0pp#
zVS8<#+&5}_vi@<bXFk}pB+daA10zXLYu72GUIg@FE*T$^g;3(uJK6bRAY|LnbbvSa
z-_8D^!O~)kN{k<_L|XAbhHHg6ZB(C&j;(0Ejz$Clb%N^P@QUX6SkDM*Zp@wNtv=wP
zhWos|DZ0%dq5E_N-ep9l3Lj74<q7-*z?+EhNrCwiPh~c)nc{I(K<bAShnW2*@3f?I
zKsEV<u|_8MQHW1tSho610zaF;&jFOcR|0&<>XsLnX5EZVSpZP0{8v~{kl$qAIZHnT
zdf%axp9d%@uSwvw3ETh>qN$|bl!TO3lc=nwl$WN6)$eK}5JVjr9dF_vZwjQWHhl|7
zZ5J?OQB)bY4%dZ(tR;#c#{i=(#c-tEHi{p^3`Ow`0HyQ40DMe3Bnen}I<?Y&0T_Ps
z7fR6=tw*J3Sof+xX;X;yh!H(C5$~eizsxBFzmmYO0^EbWUjsNbTDxmb4IS&yXj|9>
z6bsOo?7}aceWSL6?^!X*8#`y!-rG4Wnb<^Qt}(LRw9;{^Y6Yl-T_+&MTy*43*5i4o
z#!o01F}Hn6+rA>~zUf*9hU)RHpf4xfmcZKq%1hrc$W7A{bqTsNZU@~IfUL`{(%oX+
zr6n6VZGq6TVM^kS^z{1seNfv2jl{YGpv2mez&j0e`$!fz->|3T%X?P$H~ZJD7|UGr
zuA2s%(%^2|9L$<xCXfRtv%G&dNOZ~Okh`4c9k`@wt@>@YZf|`=I*XPmSbDlqUI{_O
z?Sobuly3r*Uf)XKJqEgcOk`Q6Qxc<do^_VQmOLT;k#k;@vHq2#L#z82wXN_L1zNtq
zQQCm^bO!jh(J6`UOW=2aaHuh7xpC7lvM}(y*DgW;jx3wFEld8@PEg?o5}lM|I>6GB
z{#{&4ga;D%J%EbA?+dhi2`dt2JFdLdKs-7~dB35Qq?{xQWgSWtt>feHL2#C6KT049
zw>wIuU^BY4w`0AEY5GI!uJE5MNR9#-sr#P*#q_@t_!9%&Q81uGd}N*C&%)b||BnsF
z^B*0PlUlM+#V6hxmu~u59#r`s0Vj#_Q-JFInR@+>!A(QqcJt9muhNJj5}ffcFu0Kq
zvcMKGP!!_WgMf$+lidiSQBC*-K*{pU1pW#jZgUiC^g%4gKew^Swz{o~-1|Vn?|@RG
zPyvN*IqEVzA$T1oxOr$*Nq!4Zvi&ZB|C7K+4RmA7xc>#XlHeZz&PzV+GCeS-9NOJe
z&~ukVt6TieQqOu-uY0+PZ2*Vsf0su|6>%+{^b$jGxU0yzLuJwBQuKASYk~`ZV}oJ;
zU{7gQm3PN*TrkpN5UHb4G(Qedrg_33ccJbELC#Rn$Y)yTUyqKGKb4Tly|fi~d-PAN
zN!VA&(<@IM#_suW5^DPhh$hbVW)_iDDQfAKXE0YccYgt>sDBoqbb1cp-t*C3iiQLf
zFeJd6l+sfhZpUcdE(X}f)=9BuJZ=5K#$m@ki6RPI1mvQuqD?7!(+I`TNa|#~Xaur5
z1{#%jImD#$t_G0GJNlL>={Vt9wun8qA(@0^WfzQRG|Boo0AX`Q9g%1k`Ps)BMc~6K
z+`f$TH=mDBNt%r`1gDPFS@E%!4XODeq85;f+asy@VqD)GBF}x2snn@-gP;6nfy_ue
zc+o+j;6=MBF!^`Vmp0#BYhFD_UZoQ95ZH2ipb^?nBNTsEj7uqGy7%2n0ZJ*>RQc{@
z*6HNCmjk@Jo$tCqw(L8|BHt;TG2Fq@!aZXWNcIj6MT(alTDs5MnfRt9NVyc>kZ1#%
zZL|URDzX8Wbj2_Cma@Ss3|C8vdnKm*2d6P8pI`hY8&KUg@w>axjq3KFY&TlAMT`|P
zu5))l5(zaEAgiQ%6~H@S(`+*urCzcz#8u(s2-$B7hThZ0R0sP{9@q}sEg-=CsG}Lh
zc5n1<(dL>@Lrt=<`Rq*6aE8h|Cd8oM%Pz#&ZhTH0!%j4MmP-O2#}8miX7^(!5{M5N
zy0C!2tl5mPj4-O%$kiGJiWWh|7n4#5FpKU0<a`!dft<_xIY&i!w_jSm9YWtdp@k_u
z)1r6TDCCNKIr!&!l4U&wNMatH$~!vUlb8@~w69&nu%MX^YHOw*%*t%<(M!MzJPqgO
z!A$n!HY5rBmH^#d6o!>lDZUWBGQn#TcmO~}-GKmwi|vz}M<Zg-uTq{nAhei3p^*xC
zCKJ#Hv_rGi1UYL`G{I|(UaJY(T40hukxjZ=7ri`(pmI|xoN1w{#E@G{Q$@w{8Wrc}
zL-u+D=m~ryKt<0X02MuN0?5sudow^*N_VJ1`MxCf7J##3Q7yBCG-Aop>ekAg(4hl@
z`5l@;SqFpC!E9L$&uJ{xK<ePJ_N`!Xj82jMp-3ETcnus|`AWf)(NHX6*1j9ma3r*t
zfSwT2xtQ;d4QT9;vrJ=*aX0Cc#xC94&?#%a9UxCA++hG!e84n6jCKRJe6i{fc6A8Q
z{Jr>{ZsnCAio9KtD^=>>3EcHabcaPSrySVsqCeLLjD6a3pjSB)%=1?3iR-s)GvPEg
z8b_kwJ^_TXg~>oA{Rv8cnnwEnH6|z#-^IDyY{cU;>ctJoQpAUw!VXd8Of=zk*MYsi
z-HT_){cGaQ`9!ZS(QPk%X_elWe9+YC6JuSqfyzq!_W(iS!zcNPJnV2VnGcB#4S*eN
zUmbgq4Z16^Ct=(R!mUdLHMy&z3O<pv<zVR6Fq007i`-Gx<8{?>dUJfVSvgaT4wBnX
zr17+MqN=la`|Lm}2o6Y#IRo+Ua4oIh4^UbkV~}Z$b_l)9tPQwai_3P}0Xe%6O*b4V
zQ<rvDRI?A`Bvy*e5Rre2X-d|fHG`wWO*@C|TRuA2hZBnETIH!Nv+uQDAD5uodYGF6
z)Esas#<N-MQ;ooNN5rueA+0?Mk!}uBNE&M)jddL6$ymoHuxVg^E)gJ4{t;wlK57kD
z-~6Hwce+<11A?-V?yVUk;Fl{)09}?QB0d}pr23y<1}NMYx?}Ak<T6fnbnGqTv^*-d
zCz1HUv*KPH4wmd!x{-q_rAJq85Z5YUA4uRy0JUNuM)E7?Tk9@{^GhccG-37hh@Evz
zx=J_1AH^hFXlyGs4k+gy)m=;w&Bh8@Mib5T1)J0xCechFVDh3_j|QDO+u#n*aSzX7
zQsJ;g^pf5IAm$t4dN-rOkd(TiV(G+=^Pxxf_1S23fbFn7^}LzVAl~DN%SbkyGo3a9
zx(-cQ4@rRDFI6~Fj1or%b^c{Tm4*yfY-xisn4e#d@njIrr|fMF!r{1=Sq=iqN_&?n
zmf9T#7p7eaMY08G=yDa>Rk&6-txg~lK;eW8$*)wo1p6=>kPI41#<=x_8fiBmVF8Q6
zEx{CjgN%KWj6fRN44uYKn8x4lF?a7pug40{+<3XoEQ^h!532A8&Y{BiZHC>DY)6d6
zm5?Guo}s!kKvE|85WvM1G3v$_dsmYRM08)zQWhO9vFfn6qpBJXmikBZ>m>ubE%kS5
zhg+u=v``1)W74qDyPKl}-L*iKv}bY_jdm75?MTiBsD=I<gKRFd5sd8?9BquLb#@Wz
z6%G_}fM1m*a?ZGV$zA7xj0*7i06WA(1)h(MvyJGdX(PLHtw*}sb6Gp}Zn;TSMJ!r<
z;|?YJ-9XD*7&JbDYq^Ol9Zw5$M2q&sPnw&6;trjU7Uj$DAaTjsiCQ2}YHiMb4kVu*
zfPf%h`e)w{qgP}oN_c#lKbe?NUpU;20XZ>Yxa7~ElkvbbOe}cHl|P4JjSvyfqs&r0
zD_4&8#YLjLj`RU7^M|R?Ql59bCP#ND<Am##EcbEFW$)z#=UPi6)}}Vl0cCg?V~>($
z&)QU}nn<gh5IfC5yw!F`XEZ=<_hckiye^^71{SxSTIuO&A%yuVBHGN*LhCtVO$~>c
ziW{xtuy1V-4D*&z1|_xVF_|p6LvjMAhUCWF+OA1f=;y{NvT6?f2n8jeB!GaFpvJ`q
zyG}-#8*8O$5B9;zzv3DudFNNOdM=rps>>9NCF;h`ih>F#;y{Jk{@}*9K5!&bdQpe8
z7bFg(qlTezH72I~svSZ?!BU4Ltr+^L0SSl4)$US{tnx3P5RY8=&WOpxmr+VbMs4M)
zi#e!n09cZXWeeUwf9>#!T$~u0Qm*{rN#&~h<fB}rqqM4A5(!LIeX)ng3b0SBeQl{-
z)+C_{<psd<cPQL>sW3+m;YImLjDZAGJybdVBCc5m@;}ZFn^m~4b~Hx#$TZuEYi?b)
zp_5IB2=JRkNqUM*#qUcXP*w6DtWW&-hFI-LAZeylydE7%#hz8;c;#5x<7*fYjzA+m
zUjgX#0(iu1YuqIODY?B=zrA%tege9dqv@Q4MoZ(@0ICq)NN}#TT0*eS)t39{a7S_f
zlid#_t!IA0_%VA}1r%92BK={tJH+I2aHtJoSd-@9dKlN7uX@5x+_RKB5sT1uJBgcg
zqq!A`n?R$KAlzZa1Uaq3M;gS8NTPB;qaYZ~zB7x`bUK4lmdw@K>5eLlyt@rd<QCl?
zu=gA6jUK9<Y1g&0f?>~0(z4dAOS)-!ir0>@C2i8Asy8$VEY9alxTric@I5P%@T2kC
zZzCdKUf0$^3my{H=-_sI%Sa53Xt3JHLKJL2SyLd?$g6<lcLFR0!WA0wmGX)tB<<oS
zYE+d&F<Tl1fo)}J+LtOyBYI+Ktz+4#mX2#|q$askAHRwTx?${4@z}zi7=Dv17s&{9
z%+Xf)TL4Q&xIshS2sh9ODHS;}<VxoE@+n?v3gHAROtMT+9$|~AweDVkRWsadeKko2
zX0?q#(o7lQo9HOzVCAJ-Ov<#DCnGFIr;KnPz>*O*<2vqoHp2+Iqv7^QK}ubx0#T8h
zjHJ#`GTIwSI55&6Ukh!s%7hi5y2gALJSl9pwPi`W7Xu6<HVlbCeL^4x>I_5bqU!jA
z?NKM&Hq_fY7*wX9SzK7-egsfU8GVP&Y;jP(ear&o9yD6=xT>^M`yt>|1j9RF{H9Kx
z2gX~_FlLycz#v~ee_b#e!`yEZhh~Y0_(m-lEZt^^cAV(fQ*PAhUa9^F2&-`alpu;>
z$#WGdwdL#}6-MaPfUkQ<zaNNPYu6-vs>n$tbL?QcZlJ-gMoFvFAuP9|Fc_BF>KSS;
zF!<UIe%F2$#nJ0(Q|bR-5{KZg68LLQpn#i`LhI1`XO+8$f$Vn$fZ`qVFYLlUSAk&V
z&l<ydUDZ<lmYD^h<e%SyuKe>mg27;X4C;e6g-8A*6(kkfYDfOjStRjah<}zwcF)5<
zcDpdSd+IU@q$#`S56K39OyHjktSjS^dw36Bw@>Im;x|BU=bqnNcga2Y#&Gidp_U6k
zO|>Xp(^aZXk7Hb}dV=62u1W+tfT~v>$$(ztb46rfo2*Jxp`?Ed&#81E={>&$OO)!Z
zl;q1QCE&zd!?VmCIFqle@#&?UsSW%yAR{aNC4tWxSf5wUwIp2JO4SdOUmwG~c7A=@
zy32m`-^^~$w}$QZAs@y+UCXMNgT92+;dZsKOE?vUK%M5&AqmOxdPnJZe_~H>()-WP
zdl2!SG`)`N>U8uam&qJEa9i0Tv^+~>PHpJ6oC~MG7a4uGPuXqYc$59B_sUn#p`(qj
z@`iPne8m?X+GL?WGOf>*$!$`pGUP7?afw3j2}DlT=gzk_e;pBG6GKUBX{gsZR#q<z
zp6<3g&UN7vK|AYy4+yq9F=HAwF{mS6ZR!q2hdp*w$?n3H>SmjPCRU;RCBSh6UkZ??
ziaA%^ne2U;b=Fr)MOZT19}P)koX_d&rx;K_l~F2A^DuNRn#!SB86U&ZFnBK`JZa{h
zWOU3v3pGFSsYsTLBKIgGK;d|HkZtR^@oOnRANEPXR{(u~s&YL*jMvW#xh0#W=WW?*
zF?<2<+37Z8g`SIbyD!fm7V-fa0ybdLuE%4<%ArmDBB1Cv8)eA5ZX-a-asf7iN%@dJ
zRSSejJuhi)j}axmzS-seO%8q)s7wF70LsA#&-!`QbUFdOpJO`ZtSs%)X{I5S(y8(t
z`*!`LcdQPePxdtuUM5<<>XYk|cMk;W0aP^EN#iu(0l{QGm0HeAk}$z!*M-*^Xn@a9
znmI`t8blUC1lO-CTc~7h%-8^g8)dA0(9zCVm=n@nxxQ*-V036%%ll~W=Irukw@c7d
z-$ahcMfX%<p3<9r(<wfiZp>o&Wc67}?U=4Sh{<1#acTD&fLtc?g$C6(L0!E;fYeq(
zZ#4)H=o#5O^Ie3VY$;Nxe15zhy)27e(Q|dJ7`w59l655=)>AYjShl{RMd@u$%*siT
zPxR{d*sY}gzC`^VD4ah>;^dwVd_{m3NG~<$b*B<-N?UrdV69Iex3(e=-*S>w!KnU#
z2{F>2fxjBEm+}+}+m8B!XugZ+(dz|kam@#Rv(Q-^iu23j0-Z*o6T_Khj#}R?h+5v(
zYZpXRg|)o&9#AS36;1uwf-#dXn+DX^6kz^(bSjA608l~nMt};ULky}vs<<%FJ%#JL
z(6B7wNeN@eJr!-jWAOY8!%^Y@=OA3w?@GaF?@6hy>F}o%>@+*=#I>l8${dXO-S$s(
zW9;H}D@JksiO8RZuYV6SI^m7laK$I|sorNyK91`ZShaIXT(Ru1w(1kg2yfOmp?Q?H
zJ<LFFTNZlRmisHNAAIB-Cg^cgeG}Ip28PyRCak|@FkL~i{-}^>6Z*D{<WHOPw;QHT
zT!;Dx#>2C6tvD^O?%0uY56Fs%y#wlxXXPF{ht>@QkCpUR3H*|4jbb(`sEv$2t<+4T
zq?z`%9-lz#tt639agguf)^drZG1ZwsrFAIsMpCrx^-R&`sUK<kL|;#;BtWoK7j&J5
zqy&BTPRvq1{FOlkzg^3h0-QmFBLVIkg4as6m!k-BAXRw&!!RuN6Pv`0azwKg+GAdC
zleU9TR0$8(2O`Y*{*3UESjBz}aHdNM9g^@(8DSz#3og?wFN0cd&ShA3Bd!XDNI`OS
z%FWbdW9Tf%f6v6fq+W=`cYuXL5sz2O;i$k%51cIc3>g}sMMBliBFIfk>8m~&kREwI
zP_=76CV_uXa6!#}<q*K5=zYI}=rRL`tl=AawT+nIZbfG~B(WE<M-MwG`mPk6Wg2F2
zJ(Tx2(3ZT|c6zW$5E>WnioKIad#EARj-<2<=c=@LEXo_A(%D{oZWPVj$d`c`A8s{!
z@TS3%ralqYJFum<$hv`tPk@@ecvQHgDNn%>#R+pTI0Fq;%nfk!2==m*ASXz1auwL0
z5C$+`Mp_QA7ZI#iIKaJzASn7~qw^AL_-R>_3^MK#%BXXIAc=f^V-Tx(+{TIzSUL4d
zaJE0R_1N4U<OhV>2pg*_hfwK&w-_#?@Z6#psiN2njf_@D%G`A5Q3FbP!A+^h2gE)a
z%9<HwJ`8J5v46$M4PFzp#y=9;2oMe^h7pfBo_~p|K6!WdTZbtZ3yY9>PE~`k3zoR`
zt#VOVw-$7_BNqsG=_yybRvst0Mq63?N#J}+D^rc6&0ki2XNXKj0@LDT%>NKGFmb|g
z)`a6n7>%{*V9?H+bzsu#6C93_n*A$2ibmf%-i}Th8J+eguz=tm0<73f9@QgyZj`rU
zxiQRw0B$Xn;x($TU)qvBA8oaqUbf_UO#W*Sfdbg*hpd*q<vg+RVhGK4(g8!mXkfaW
zwn(aI3%wmxFlj6#2c(xvRvX06Rf-EH^8@f<O0g_^$U43GC-a>|V=`4HQ<LHvFt`d7
zk~-de?PD7F=b-s4n)A_og4uz4e+FiOqEvh;EPGhn;uk2f9G8x%c2JIenbi{6_SIm#
zBN(gpGGk|7Tg^cmE3q`f#-QkfTH39s@SX-tfw+nB;OPncAUZd3+8F?EfwdGn{)-6U
zBE-r?c|E);p;<CC0V43*&SD5gQ~kzkbWO?KRrMvPqGC+q{|Utub5>ZBO>lclnWe-l
zT3zoe3n;8YqbO~~(d)gFmEv`nio&CKSh=5pdK(f}EVkmB^*6mKT)+**2P>RVJ&03$
z7{lu-Y2J-t;1vJH9HI@~1g(KEN!nugN;FV5Yqp9|GRS$rLBKn_T-ns0yC}8*e}Z#?
zde{GhTdy&~a%)OgrFb1Ir3TH5x~CEBxr#5KVI=?ij!d-`Guu^r75c4ExKc|>>i}wf
zaY?HYS;Q$!@o@}a-s;Da0uQ!M)W{@-bsNYrknb@l3xDT`_tX=Mj_uc!k!^O`)h!?h
z-;8D%Gat_Pr2!$}LB7PM+VPRpdm+a0B{Q~&fP3d7NIh>ztGGuo;8!{L&0U>;P!LMz
zxz-=GuzmN=Z)A-?(c?F(gb^FMq1fMm+U``2yGW_=F^mhmG=Y>^y_aEJn^XF-2OcY)
zzyh5fB57^!PMuU0AxeGy-rDavS`QXd!s%dvHw5va#KlHof<<<EE%AS;hLz)Hzjzqo
z;udQf+`i<WG|=1OQwjX11YVKAPaD{H87;|0@fNw8xBtZ!;Gs}8rU06S246)q?M(yw
zanoSG%Hc}Y2I1?P{1b*dLH!pJ)eT2+uYw5j>(vSTd;+gY;I%+4M|F?XgiHJm3u>l&
z=Hf|QM%SS>McHu!{KBHSw-n92ie|Rc!7S#MJA(TCGdiUo3ZMtCOW^eh{36DCIqe35
zRmUKj^OG<EY>F+Rm>{<0++CCl0YxdT*SxXulk@SmQFFxZE@z`_7yDP6PLKzlZVq~>
z2luOexXiRIXiXF$F|j}-eu9;6w2O&`-l-%p3dN?<u8N_`2V=$8ZLG0~X8Nju-lShk
z;Ef5qDS`hARBfVART~pD3f6?`4Opx3CTlX9wDC%S>r*-D#&sPHjsIqtRF$23tx7so
zEu|YDpMP^{d)|u4_Oxh>+OL37_;5Ey?F&k|gJ?9}Arbrr6i{?-PT(C0MD1uvIlqv=
z!=+&NDQ8AtKaImW6ScU_2BH=NJb1J>X`0LIFEo!0_S&D8!PAk$IoqCza_@*|A@`ll
zu9=L<8Gx;mWzB!WxEuP&O3&YUZQF5=gVBXl^=^QAo`@yeYyC}tGv`{vXTXgSdKmi^
z{f(LtuTq0g612$zH#aRJ8W<j+W7<-9Q@d(A23R6Z+I?EmSZ%{29M>Zrewor(4I=RX
zsvDv?>`b*_F9p;@g9?t{jTP|`=zP0O`@qKPBw`ICEQXl22=lV^t%OJ;;<>Lp2&0YF
zFgZoiMEW%RP0)NRkog5wJ71<V<$R}oxe(m-<^_D&z^#WVYfa9Bgq+~_(W}7y0l=Bi
zJ#7gaxM6L;wvCJ0jbJa{SOMGCxyRtQczOl^?=~(3lhXBYurUSGTlErDXV)-CSXlw_
z)JtfHrN(I3Pd#8)Ep|gfrz9xnfDe5;v%K$I(9C9PtqIXqdOL*yq4?(_bb?_wMro)Y
zVWz^K&p>qa@niIs!u~3TioW1}ImS+4O=4Att>O!+jjLd^+7SAN(O7~g)fi5CT{Q*i
z!q!pFXc=7s8jY(XTB0sAUNZ!+04O<_o&20aFYZ@If~_C48M3uMxNf!e<ON5zW_vJX
ztRCsH4^7GJdYUG53|&bN{5L>(;O77pwZ8yZ^1!Wj*|<IA^sV#k(w`Ma+fW$#mkUHQ
zT_a}eEE4fJ4tMlCj%(bRY^qZp3TO`p<hS)UH|v{YjhxqQkTRYo=GiKjug2ZL^yhd0
zOPE3K+e>mAM*Y-eKrWMakq^UQGMTd`WcI9KM5UsRs%Qa8jS(K;DIg_Kt169cKmxP0
z5B!;3OcEHWdbL}Ls8Q)vpmu?w(h&XAz~bj?*dG8Y8vY1S(eNjL)f)D&^);|qHy)|f
zFpel<bO5<4=2OeYPYh_>61=N=wGpEdO7#jBm{_lf#(H&I$f4gGT8pV#*6im~u4sjW
z$*x5x{ci)M%7toQ-(*eWHn=?JawSVWh3TqXe+F2}o5$?3@py>8$4c=Rxapk;P|s9T
zC=t0K1GbwtPs8Z$VirO~7B`<xujKBQv}#Et{^b#c9QMwqEW*6Tvk1xjxj2V6SM~43
z828t}RiKtIy%t2tnbcgK-IJvGj7{PDsvUVNwT^nC7L4<_6tV%nF;G7(ve6zE#Q2Ds
zQrFicTSEQ(jD+4z2mJ;3Dk-#XAFgTQScT$C0a;&3KFnrD`={vi#RJx-Kit9+!%r0J
zPXn{V{xzO8EvR|@w31xG$Mg?acX0J;!+&XsKk%kmqhh9Q*Ryu%*@f7D!n&M0YK8r;
lH~tMQUD(@Wc1DSAdlg)Ott=iI^slM9cZ@81C;lg&{{v%89Y_EG

literal 25921
zcmcIt3z%J1bw20Zd+tO?EU5}@2nGog5-^556q*2ez?A_i1PQIulwp$G!02QqnM^{!
zsNe%4h@b+IA|jv=1s|x?S|7y+f(n9)P*A8s1Ql(427L6f{{P>vd*)_B_`c5fvF|#2
zuf6tq@7FnDXrR?MxVnF!mASus!(ji$*6{jPR-BsUxz$=xtQZ=}R<%}V#j<nOwoc8u
zd;>dmp)5A`4QIuYp`ih5Wp%z{L;t`?|6rDn3~y*<;c0c>fKey4K_lBJ`m&ljvRhf=
zM+Mpn)>=_NacHD(q<?4-6?yTMTi7tYhM&6V4GohVYDl2Lat}V2#R~jpC5TQ1v<FC&
z*YWM7H*d~B^~EIpysW)(`7AYp!o>Eb$F^)s+9+Y);3^<ydzLmT{>s3IcmOx}8;@c_
zJH2VsNNy_m*sH?FtmSG%zrEZ0J+|ehq>X&^uUR|L-&zmkPQ0{nF+P~8wJtku&DyN6
zU;E4R_F;~s^5&pvlFVs%jbbs!HoJMET@9yt$|(E37`^tTd8PpDBDg=m@ls4T;7KqM
zJ%D|?zzzQPv;V5>Job(ciXp0NKY2v|>ecMfLH`;6tsGkev`cuz%%dpGUz6kk6$?Ce
z!R2ZNjTzKHYg7OFk@ZvpD)(&^OQRZ4!=a>t>BL~g41fnq?nbc*PhJhI6mKJEnI+Z)
zdgXyYn~0)IT?vxlOn~NUJ%jSDxoqm&loc!cEcn0{{u+&<XSRZYL0q%vIeO-hb#KCQ
zDvUrabb-onYxO`XrAF!M2GL0<#4(^?vw8NA=jgqD!;19?{KaU8l3e%TC#l-#9u~B1
zj7}k=8V;P*L1;dTDO3eJ&G+7NnAO*F`@`U?Hw?BmwT-?csFX@DepXwJvjS+&Y!qi^
z4M4}BNQN-i?g_Z_qxcJeM;*^pW$fJ~gH0fCII=q4v%1i#1FL-l1EW|)zk?ga(fG|K
zr^8Q)!<T4GhsU$&P%=?Z3)-HR`tf@Vv1XcLHgB!1xH8Bbj3V%hK}@d${eA1R;@h`n
z%2i7(qxWVR)NM3+?Kd&DT+d{X)yI2arYuLVJ`;n;o}RN)tp=Qd=-T0-q1C<p!^16j
zq3Fm(&<{poR+1O)?<t&SZF!C;q64l4ZuY9uyP?m}T|PsPFI|`%ZGkkK*vA+o(y!FS
za~QJ|^-Yt`FP)M{fKNA2D0n7Lw`zz1HU@`Adiw`QhKJgO;6US0P9R<CLMh`c)Uqi=
z71EoiwMP0<H7@~fb|Rb^e<yXLoP^?J&m&!rsY2=Zb!b&mem%ewIsO2^lMbrk2kvPB
z!1@+J6tw91fJ}Gtu_*@<A2IJe(QBaJYKlBx^ZMT5VRIVGn|&JwMlvX5WVnB0e;)_T
zYIKAx=+EJ5K<Hbse#7vpHg(A`(dHA-qs}hF>`ag|pQNN^CeYa!fWenB$vIW7vw0?Q
ztQ8=H0CH|HEqEAJD1B@s4o5pXf>g&e)}DjfDbrDs9ahT83AWHeh<vp(x53&>YnAzF
zGu>|$b-kfFJ#Br9T0!<YXm5qB&Q=cDN}x4@Il#pY^*pf~SagrbL9J7zRQpDtm(w`#
ztjt@TT|dN1Mb|c<bzy9-`g&Uf{mBG|?1jHNit+4x9zZ!e9jZPJ6*r=|8ifb~8V{=d
zYu5IT4EGHpPlYrPthEw&iP^RWvl%4xCNSo6=(iG?;M*ej_6S}8a4Qim6j<~)DpT>y
zKo6PpEmq?L9c;GN?KY>~pc-vLU*jO3Boh~-S-N^>1TTr;y8w#eO96h-vX^6+YP}AX
zO%(LPcK$E2YR|v%zI&SfB8c8fF5d%CT)sDgmq+jlfM89Db!%i&T8*qSa>*}M5pv+W
zjeutrITinLDJo&LP?|w%+zV(mMDDI49~|PwHZOh<4fM9?!+~~3FMa?$<i+m?D4DMT
z_<&@H956|Z*JSxVV7LX7&ynzTrJ^<3ApynmPjGFQi1rB{t%OGL<j&W!3x)h(1Znbp
zSbIHcCj@QJ@2;T&NznNN(|X8`AFygmK#01PLpEvktsP<(%YN!7&bYNPq9n7A0fXXs
zf^r3@_?aCLeJ&XCLssL)P^KT1Fscf$)q`KLQuZVte-!j(gqtIH3qV=vV*qz(qIxsn
zOiQSr0gMq5xci7zO95~M#<V#?+X^JIH`uqr?J_}a9~7D<J^@f{eKLZ#8kiU2g^4bk
zGOjqQZ)2;swQ22emPgmw0iDXRcXWfm&rAh+CeO0|XV5ZVItSlroNHo1UAy)_ZZ%H(
zses9zI(0zw&kK}Vru;KN$@SR?{)>TmVJu5C<Ha#5$5~~<HdzVIcAH^1R)$;ahXyvb
zW_Qf+76zKWFruUZ^fVp(3joCt^O3+WS!F)i23NY-0i>Be?mll1-T?<!jb5BZ`_4wc
zOzuaBeC!R7W{|PJjAxDel?Z+npnULa0=bJww6Q(tDRIPOJeRjyr-VyPsyp#QX@^`z
z?TEFzFtS+tMg+fUV1B4l0sO(d76tQF2!uPWrZWCmPI4$HNZh*tYS4Qk_-zC8L!rRD
zf!gsJA5PG5{BK#c8-Hk6MrxB^$tN5;BpYQ4qh;WIATCzE15mZ!Rjps>?LgwrpNGnr
z5Jbcq<6dAeEqY#{i{L0SDwd8Ql8vvpt8DRoG>Ml7BFHJoHX$z8YtHb)-fwte*y^$>
zjJ^`o+zKd;OabJ&ejOyAH7+?f=Ht*!ndD(oU_kvKf<KJlBL?QD5aCgP%Lx7m;J9d0
z+Zag$+oNkYIn1YWL(Q7ZaO0Dj5oNE>a}i6w;QT+|p@fW>FX!y~D-5`tq<m)4;{wz%
z=T!@@%ZCiXuOIAWW5Y<YI)>rAlBk<H$jO_x1C-f*Vo*M)Jt4>$3JTdw^ZZLuVLiP)
z6_DX^0`2oB;LtuHCp~U8vh@0M)?oF#7&x7eO{C)esp3h%O1ze4`8m51d<vkv{uclx
z(=P$;KOH5fcR2<g)!qV_oOCqtOvTQp09)9OqCHH0W;I^Ne#Jh9AaYzB^UTh=K`ly?
zcyDYW8)}J_$$GH_jsHTS{Vlx33IA(=67Dwu6_UR-D8G>1eg|+%REgX$qP75zgkj}%
zM510~XYXtOX}CP#!9r@V)%$F0O42MOA;!~L8!M|e=9DHepC)RF@);Bo^A85)S9#CN
z&sFFt++ZiSSm0nJ9y0&$t<77}HU-B2ZralN=NFn)=g6w$zljkO+p)50yFUX-Lj5;D
zIqv@elu-W*khWt!k?nH8`AwZ{*Q8cj=q1}>SlLeQjFv9u|7!t8hNN$AP(*BM&}5&t
zJN`|fNm-hpj*N7UfXcUl*}P_jbdWO(Q3pAiqyx>K(g9@1KgVw406sha1s7xbFIRj)
z+}1kVXxZu`WXLejU2lXOQ(TubOXho`_Ijr4>i|-q@lnSTCA82E+nk~~3o8${)~(*j
zus5JD*P}U8uZDd-YH!fudNp9<%r8DUdPZ)jcq+CnWOF=eVB7edIgFKPu<R0&<B>5S
z+mD^ensC4{9}@`FnoaW4NE1&iWNNjtl94F?A}EB?+VY7&U;yNQ8Nn9-<bE!HA;7J~
zeGx!T-#ONP`M+yoIz8Bl&dfqCR~BcXOa6G|WrPegQB5w6iRm4cIcGVa81lWWD!2vJ
zG^eAQ`aloMW-U=H!P6l5IH<|~@-2}Aw<JLId@@6`$i4SPt+X*Yg8KnvI>=uPP`F^<
zwi_t-N5N3YA2U!v?Nz{|x+IZjQURr>9+p;A!1*MoV3N^mS3yS&$N@V#igeO6RV0&M
z{x}#Fk4y?dK?+p4NK#2v1>5G^DL5;oFA5=$z2rRzLgzgPaX@yP4v?8LpJ7l@W9`8J
z>ukdsAzvPcq^>z+)?yQf;5A+su*7rIpsb5dnL}+^0sm2(Bt<1<a9C(hvDij3lHVtZ
z0}QQU$LsEdUH5T5S%j!v3Tn7USwa9=%QliVJWzNy8&TapY8lAD;CfPAmiCyx6qVBF
zOn?Wo_GJK-er6d|9KhN`0UoH49tVcGXz^+SJG${>n|XzZd~c7aSta{<KpLU3eq~T`
z2%ejk&G1_sLfeuzr7+YgYP^EbA<W>stqi-|(dr4&O7huEkS|^WqKW*6;aTz@4p8#{
z4M2q=ac6S55iXr57iWeAlA9Hx%AP3vhBtqOJ-7{@v*^fBZ|B=7vl%zNV$<@xqMAz3
z4U@KDOw;lmTIMJWC@B^KloX2$DvsmbM^07CGcH8+30BxLq&OSDuw##)rPFG~B6sb@
zrY6e7DBcuDTD9LsZ|Waf(`$EHE6*D0Uy1EUFos;zW|&up>`h_X@BX4?jFEFV>=ZhK
zL_|ebz`@x|NW0QclgMPU3&=C6lve_jQjU!voS}FP5snAAoGV8f$?_~}dcE4UC!nrv
z11P>QNb$0O!M%PCT}Vmd%<q13D9`&V?k{v9D#x_ARmwyF+j$%Qa3Z<_7h%qKQ8&LE
z<s=l~I(6PtSV>uyMetOB%8P$zP_b^hmHE0(WNMu%>*zGBZQo{tZAdIQn6!$sMGPo#
zm||0fLX-GtIoCR^@SSR?#_quh!FpD*Lv<C!N;aE|_N<_}i%qohpDF{AQWIPy_fqT+
zIkKy#qMXm9rK1pKW@Q-2<%n11vR=g-P^5B*1Js^Z8If!xBhr71^9@ytCHf^6ZeAGl
zFR0!UNU=Y8@2C)x4>L9ruM0qXPbB2QT{;)Kt)n2A6jOKV#j~>h84)Bwxf7hUSf_wd
z-e=4uQR=h9>A>{s-JRYOC$C&k2{ejk=~a<|7C`Q0ifaHmthSSgZKl~dXmqP`&&Nuu
z@oaR^Q4hP!?Z!`xFb=?*!n_|XQpxK8&YfmO!baW3b%&`W!VM_(5ezQ2>eM*4TS~&g
zjAvPmI2^Rim)nml2HqHlB>7drfcb?$6}N-z1y$xl05$8b1*pkvok7+Yk(Fa$+s>j4
z%&f5opRaIjhRf<IFJa_t5&FtpSV_5DOHc077*KzfEn=4~02OxLI>S~Y+3obv?snU@
zVlFwh+a{k(THH=J4THu;(3Y7vjg`SnITqN(U1lbr<ddhPgc{r`36Fj*be5c=1Kj(8
z<iZ0GGLdZQPI&J{t+OT|WJ&xMcf~;{FZ>~At_F?7U5dMbPj_J;#UXf?Q*Z>e5D}*?
zrm4R5>xWi`Ng|y`q;Gd+7&PU^4$mCXZV|xNn?YEbJ1>Ig6AVf$9%-P0!t5}>4osb>
zk4V%=I!Oqz&vxrmpr8_|fMR=8QWGung+3K9msXn8X=x##1sY;P%9?NtX-FQ2$0w~>
ze#2Rl`YoPBN1l=hoz&<&u$WZFs~w?}Pv8{ydnq4{yh6VGlnSqsO<^Ax6bCRNIVheo
zhzl*spP$lBGn-PSNw$Mqq*C1*)lJc*3i=Xd3;Li-N<cXjaX_>9Be>za4LJBuUP>YD
z8F2(EN=0d1@=MS$##e0|o?#aJ*2YDt=q<4Ti5#5eBMw=ofU*hkI11m4FrN6zMRGCH
zk*_)iRhD}<z=SV4PT*@|g)eptgOab})-n02yWk^V$%RpsFR>K)x`KRR_&D3wCfQ?6
z94b+60G3`Q>Eg;Ozl=5BLU;*z3}w`SO!X-pZ^bjyK=IY7ez6Mk)fiu#O!;0)Z5lAQ
zg(4kq3?VfXdTG3W0$5gr#Fj(j@olIY&o|UlB3_AJ!3jtDHjE_il1Z;Xn1@2+ydR*G
z3*bD6lVchY8GB)QXY)v)r@OjrZ+1eVsqq5<l?bmT2+eS&&#~{V9qzm%Ka}gA>~<iz
z?Wrb=Z?T41K%S-QJFC?`Ru0DqwIk51PThFsUV{CVPguDSNJ%Ap5wh+iaHDKgw*uq_
z&`1IVyPp`i$5+OY1R)|Kt87p!33yg^XHwdm#vqr8y4oxAL*cLaO&COGp_dB$2y26d
zYRl}ocB)tGvdArRUG0=88=m!|L=8I4Ii{qEox~G6(HiOmN~eX&w5K2U)Ih?uhG(~o
zXy>D*B|)t0G;WGSW`e?ME4=EF96ASUbOdFH5;A|xiqsJX@EkJbK;(ydaUGT4wG5Zf
zCaoZ_E#;<jsv<X{ry;G(Zv|LQ9Y}{Y@umED4Y0Jfclq%a)-Yco62_P=q7v%pqowkv
z0VdJ#CN;Tf>`hcc3`KVID$3kiKKd(FAsnxTF{TOfBWw+7W&T-!RW)p}x|%q{U^Sk0
zsHZaMr_d{=zUm96=#*(Lk4l(}N-5!U023u}&cT)j^|i~Ogp4~HE{_;7%0d&+!rfbv
zuT<$%MrS1n2TJPa%a0u#*B^dproceT{a*w~X0x`J-D>m=CI=RD2~T~LBYNs|L)uN*
z@yk1-eghghQ15JDAdf>am!WnCKrP3&5JWN8i{II2fpRkniOuPwlh_P^3S)TliQg;9
z@>4;Ei)o5W&taSbkE81qo8;|6;t)F^;wvDpwz%1-jNoQfu4!mwDd28!pqzaVL8QdQ
zeibUU!&yNp^wS9*U#D+UWn{OuA>h}TNZ2V+$}YNZiQSnHs@=gX7o<=a(oFTf&}~w2
zZfk$F+XB682P!7e3%(0bO88y`?>De^8yUPV7>en>_AMp7Q40#cZ~l&Tb*C#}Ed6jS
z94eBNs42H`W*SKB^FZY1L4sakI#{jhySR&FNrk%Fm3^iL{O4q!NwNE`?PHsUU6|*A
zKrS`U52FqqiQuCK)~c_*awlE;h0ODPAiJd-pm2)v1A9o!gRi*8jvul$12mM8;<NH4
zz34}1mlyq*;25Tg1eis2X}|$!HC-E97VQvKu`9Cx&)qY0l>tfb*#%gnR0qEaCEBt|
z2{<9vaH6>jV?Gn<GuE_>e*$Err6(i!Qv++yq_Gw|hXqxAqU`z~=-0`vKe6i6uI{VE
zo!Qo~?WI`IV!Y6_%8EZnrI>t*;25U#)Tu7rijW+icNKou$Kh#BTL0Nu4}9GmyVvnt
z?T)%=GO1%1W=l0f%_~Lz8l<F=-$d}Y2IfU-Hnd@LTc0aiadpzkR=+Z&#8$l2?+}GP
zaX(E-86k8garJu)C$3m4@M){8Jv|)*ypRZ?2(F|_Hzb7L0oNZx+dI+t%rYF<FGhEJ
zchr5ZW%s%#vu5-a8N<+h87F>Gx+_h;%jafg!Oj|%GL`&+BNF^0KwTH|a9XE=f40i{
zu@bRC3=|}dUc88^_ZUz=9#fZN;UF|!fI=@{wg{p?Cx?&6pqOXu!JjvCO)@lWpADLw
zs!EZ#VVcZNiUPLZlD-T>6*)%XyG2C-@L-Cv86a6XO_cnFuKQ>g&A9olFW0pm%w`{t
zp{7rpeu%6jUG#uZ*7DEwGrR#RS2y)DfTGJ=W)|K<XIoH9UY27y7=`!oQ`La;)cR>r
za=R?mG_7wsxzMA53nmB2KMn)Yz{T?ns-IR3CwN<Z9m9#b>XiBlI6)Fll`n;(^H%Is
z9B2KqS&*|}{u57})v7kx9IcB3muwbkMLnsVDxBq2*69t2$c$InW^ZT2XMKp=`~`*(
zH+un;h9(+R-<)bF(KgU71i}SU)}E;7kb8>fTeS~&#rlT9)k6cT+TOid%HHXRq;#(O
zMHCy1<PXQe?W9_!)}8d;-RRAt35fP)_E|vbn3wh?_#(7RI!!~Y-N!2H7ae3}0sm%b
zD?qQrqiuE1#xD<$XA@d5-G0(r<PlWUsCvH%?pMEB+|!igjQlD;jBw<?Lbnm3MJe?1
z45dJ?;t&wvxnBKh+fdr)Q1(~9x*Kixk~l|if+t@4CT|lpF$@D!ul6Lg<LZhW<;$H`
z^W_zO_(qSkih=4MHYNsJQaG4M?vQoNe>bqOYpZ_<-cz)!;K22d8k9{zW$g%dMUk>=
zj|IJv;`@(CiWi{X%^9f^%?a7j-m2*2M6!VOPTzQmsiGpOlDdXQA5g3xS6W%npX5aQ
z+p}|`mjL8it2n@*`t9-y1M`RRd<6=IJ<dz$JNd&wCwd)AX|rjV*)kLy3Fve1RKFtn
zrM(;^zi(FgrUQ^~PD{(sE<Xd^`W>JY+!*f|(V^?#2&~9FHv(^bw-vP`QPRdT551)s
zy-nWZ_F%<}4Y!kh#xf6Oz#^l55sKSO&^Xu%U7hNED8=eaQOl`>XVAWb_L=pII33YP
zlGt^-2a^?@>$eLDjE+X~Vt^ZY*+6Uch(A2n<kR-rj(w2QM@m$Kz53|xYh@mLCsKQf
z<U4-YrFbo6mVwdT5dBH9dKxA5v{%&5<p8|S(sjJ@glykLBMHe6B&^B^s>$bjBPrTV
zPdk0loxSKrT2>QGXzMw_0s}lPDh>sx(13^6e@aWv1NaMqhXMSZcV5fhj*rsGID)9*
zg^=8EhlYuRNy~=BEL4AHSNMrytWU{BbAGLXq+iwzs_*EwQURZ!gL2HFWzC+-974Dp
z%1)E)vDgdjDOV~&7<nS4CiGG+p(I;~Z-vJHWgI^d&wJu5!*c<Jla|yS<#_Sz$(+xS
zjVwoj3)fC1s2MJT<V_}9!VZwDI68vI5S#&_3ou|bgXjhZIA@a;x(wQc4mop2>XKNN
z*eS&Bv0gk%ekWoCs3l)QCXdB48BjP2WMVBLaml!j9Cqe*vSHTtBe!n?!78`?b_&bA
zQF4C}j*x<y8^tPiHVgFh_Tkloo?iE5tb7XY!PTr@cEXo0y(@5P*wed`Jz<D)PB-9y
zn?G((dbPRuTeL{TS4Hr|2y&Go1WZvSH`09hw44VI);k?dgNi56{_?4)9JYclnD(v!
zlySk3q9z=<{6^1K@u2l6kFa#=gkW!Xi|eqtP$>5Dxe+OYRr%u~V5ygKVT!_wjB-&G
z1suXu<>G2fIvP>38c-Ovq_23a!E-dZmZ@Y`S^PZ~_v7rp^5_Pi30mR4>e~Vk{mX^$
z$KtD2h^oHy&c9$4CfqdCUkjMXoGEzATb_VQCbq~InYDEmnp!AE@%37(blj7#_^eZ_
z$k*cbp<O4?Jg$>6nqv(58b4@xH2S}q5g12WWR=-c7=Caiz~TuE5by7!HS1`G)khl~
zEwttt29&RAXTC(G-Hrnx|2km#W}-Qf9z%%b=mo5NdBe(r&&a-RIUD6UqkVAqvLS>n
z{?!USWBui#TJolGVo2ptD0UJKXj+J3krmQK6h*6PF8@b60XiMyg9F^lBt4+>5FY<=
zEIR<<44{sRH>-5&AIo-Pjlq<f*ZNYD5{t&N>eE~p@CL23IB?+-Tb2?gDPK1gCFU@?
zYzdbt2mG{$s0kllgmj$TTkRqpyELmQlADp3VKvv|TiKAcSJ`lOFVT%MWMVnMe5)#7
z4u{k9s%*;+0$b=LaCHRFMCHZo)(`L!=v%(yJ_7(Qbe1M%yad!Mrm0?a01Mf6pdJOK
zDSzWFtzPjxziLaMA_a|M|53>leYhGJW%jl-OOBUd!05@!IZaSF7DbO0`9tkEngVN3
z$Y}RqpsqpJqtTWAq2=us;G<Ky^*}3`e?^KxfeErasWMW{Dv47rLo?q$h`HG@f|hF-
zL((B%yzAubI|*C#UylO9W=q>yNEGr9z=1&dLmZ99EiVWDDB}Y4%Krzma*tP;8WrMo
z3@I_FUgSNsV9ix-Mu9a(dBd($wbigXx*HQwxfKFe)SJu$AIBIg+m*;9PG-up(A+-_
zLxedt5#W~gj%pbrv0epoh}H7_R%HI4_u+>Jqmz!U*A$T*R@&7iAZTI}TfTyk56!yN
z!0f0ju_4xOj39IBMNqTlE_9p6Z>jW2ic%3G%xzQ*4-Z_`xq||qI<dM7QrNnC_ZPB8
zpq%R#tAybjJZ9$$lErok_Xbo-BKU~|-xxtIt%dMrv}<vC9zj^F{08D)J0q$G-k3FG
zCG#FD?VzT87Ovbe#DLQs15bebc{(?jqcpPHbBX&0TDBXH<wb7t0DK9G?@}diHPGqd
zZ4rEX1TTo-g+P@i-vRIvnVT!}@^aw8+~vc7rl7!Q6211)0seMCf4k6u|J<f{i{XwE
z|2cW}_bBB%!GY`w*&X<<2wob&%g~;B^<0U0E>K2!HIToFhG4pj?IG}v4e)dG=6Q)X
z&pQw!B=7&w_n_?jK+5-Cv`aqPK_E`>TrCfSRg1J&&SSUt5v&>p-faKsuKi({@^YU{
z;M+3p9*PBzqL9{m-<acMe7t_tJ7~L0ECA@^#S;X1NRu;WC<oW8D}j`0S@1%DU{D2-
z7+8CtE;z}1>|wN`cPmIR#Kp;~O0LR@1TNFy<gc$pq`VJUty8JeI`#O$SbH7XwTQaj
zz{b9#wChqcb&GXzV^8#!N}mEa64OZ&&vg`#zrlD?X6IU~5>9f?s3~oH6n}Xab<eGs
zbWgnCwU|~$EAzR8T!RbhVjH-Y(moQwk4Et32;KtJH00bw0t=50IX97LRm40Kq`1k@
zgA}WI2Wc<W^scgd+Ts2c_Ajd7bYwB9+L`ED0yan9%Osag?ncEV6jtd@H5qz5)8SCM
z^wSwnz(J3h^n_0W)Oq5q0HuIW0h~O|3i?uG5iJZi(?88(A1e0Xp}~^`EwVV;j)=I!
zk4B$Z0BdShjfqB*bo$n$(PPbnYUdFTzl~^cxNsNM1Zz3geNyTIKub};<M7*95{^Kp
z+hbe@HhLn9+tC7-X1Cb@^wDGGa}BO5=b*LG1C^5{b)<0b_3MI9SfkFgJJ~W`FBiLQ
z%b6Hmr^T>kgFd0lkbgr{L2KR)P$v8`Kz?)-mxPTotge9_NTUy0skSU)Gjv;LV&T67
zpsfU~+vvq0$@4<5V=|`K?8PXru?wif&#Zv>B974DOO3@|Z(p*fHoajQib0UZfOCDj
zzPxt}XlD8@YlinW>4?X%bO`xBpHDXI#$qb!4)m1Ue;uH%KJEmVxV=kkbeI>Q?PTU8
zX7ye?`!`k_{IpzeC!dZ63lN1P_r-dDH9Dz%)Sb2-i5_jOa^VdD4JHwFq49Ykx?$Q=
za4<UgeTCkPt+sewf6aQd-R`yPdhCS5<idGfH(nOYY1*Nh;VQZTbgv(wlS4<-`Lw{j
z0A+#u0Lp8>12C}wRy>W%d`!RVAbWJz#(rRTEscJhAoPz-1V-v7pe0<#VMoucTH}hS
zQ*MLBpdAiK9?s#*x~;E_*EGoe+a2gww5;It)p#EucaH}!!SsAzmhf#D_2Z*Pz;okD
zjzc$q@^;2^wlo>KG(?4>yVAz9xCX=vJh_Y*;t+HhJU6gEt88k%Z8c*!M$BHFW};`~
z7)cI;eHvWDDu?|L?8qD9n~=q$sIBI(Pg`B%G8CVw<S@3#V|W3XKZE|1vVj?`af!FC
z@)a$e<|}AmbiN`Q^VOw3hJIjZZK`UUv!6}6iXKo2A!K(=WpU=_9c<%Ln7nul?b6ia
z0F}A615DxunXKWzJ#E~X_@7sS;)bIsr_h3U<{kRZe6Vp3l%B6+B7`UD=I9~yj#9M+
z60eu#a#%Z`JsbTR_rWC#ep1Nb;|8;SWAJhJ3|yv^<R4;)uTOx)A)v|WIe&;W@3z{;
zgDCEAr`CADDjhW+obj7kCwLTs!AYk8+vK`_T+}7Ruip{To26CgqfeczQM=19Bvl-;
zP<SaI;|D`bCdpNWJ4L50J`9qFfCN(v7bf+4@Z4qpHSROMD0%&agfDMnFvy`BKLONX
z`~?;LJPACFL?t3MyWza=|JbVX{G_$^zZh{ZW9h+OB+CTZTj2t1W^quzdt)_k4z7A7
I{<kUr2a_n7ApigX

diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 96ac9e016b..5757cc3ea1 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -15,6 +15,8 @@ MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(neq_fn, name("neq"));
 MK_CONSTANT(iff_fn, name("iff"));
 MK_CONSTANT(exists_fn, name("exists"));
+MK_CONSTANT(nonempty_fn, name("nonempty"));
+MK_CONSTANT(nonempty_intro_fn, name("nonempty_intro"));
 MK_CONSTANT(em_fn, name("em"));
 MK_CONSTANT(case_fn, name("case"));
 MK_CONSTANT(refl_fn, name("refl"));
@@ -24,6 +26,7 @@ MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(eps_fn, name("eps"));
 MK_CONSTANT(eps_ax_fn, name("eps_ax"));
 MK_CONSTANT(proof_irrel_fn, name("proof_irrel"));
+MK_CONSTANT(eps_th_fn, name("eps_th"));
 MK_CONSTANT(substp_fn, name("substp"));
 MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(eta_fn, name("eta"));
@@ -62,6 +65,7 @@ MK_CONSTANT(congr2_fn, name("congr2"));
 MK_CONSTANT(congr_fn, name("congr"));
 MK_CONSTANT(exists_elim_fn, name("exists_elim"));
 MK_CONSTANT(exists_intro_fn, name("exists_intro"));
+MK_CONSTANT(nonempty_ex_intro_fn, name("nonempty_ex_intro"));
 MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps"));
 MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
 MK_CONSTANT(boolext_fn, name("boolext"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 5ca3840e57..0821e5c243 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -37,6 +37,13 @@ expr mk_exists_fn();
 bool is_exists_fn(expr const & e);
 inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); }
 inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); }
+expr mk_nonempty_fn();
+bool is_nonempty_fn(expr const & e);
+inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)); }
+inline expr mk_nonempty(expr const & e1) { return mk_app({mk_nonempty_fn(), e1}); }
+expr mk_nonempty_intro_fn();
+bool is_nonempty_intro_fn(expr const & e);
+inline expr mk_nonempty_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_nonempty_intro_fn(), e1, e2}); }
 expr mk_em_fn();
 bool is_em_fn(expr const & e);
 inline expr mk_em_th(expr const & e1) { return mk_app({mk_em_fn(), e1}); }
@@ -58,13 +65,16 @@ inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_eps_fn();
 bool is_eps_fn(expr const & e);
 inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)); }
-inline expr mk_eps(expr const & e1, expr const & e2) { return mk_app({mk_eps_fn(), e1, e2}); }
+inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); }
 expr mk_eps_ax_fn();
 bool is_eps_ax_fn(expr const & e);
-inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4}); }
+inline expr mk_eps_ax_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_eps_ax_fn(), e1, e2, e3, e4, e5}); }
 expr mk_proof_irrel_fn();
 bool is_proof_irrel_fn(expr const & e);
 inline expr mk_proof_irrel_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_proof_irrel_fn(), e1, e2, e3}); }
+expr mk_eps_th_fn();
+bool is_eps_th_fn(expr const & e);
+inline expr mk_eps_th_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eps_th_fn(), e1, e2, e3, e4}); }
 expr mk_substp_fn();
 bool is_substp_fn(expr const & e);
 inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
@@ -178,6 +188,9 @@ inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_exists_intro_fn();
 bool is_exists_intro_fn(expr const & e);
 inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
+expr mk_nonempty_ex_intro_fn();
+bool is_nonempty_ex_intro_fn(expr const & e);
+inline expr mk_nonempty_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_ex_intro_fn(), e1, e2, e3}); }
 expr mk_exists_to_eps_fn();
 bool is_exists_to_eps_fn(expr const & e);
 inline expr mk_exists_to_eps_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_to_eps_fn(), e1, e2, e3}); }