From 5bee259a00bcd622e4d6c866ad0b4372cbee788f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jan 2014 18:06:25 -0800
Subject: [PATCH] refactor(kernel): remove unnecessary universe

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean               |  38 ++++++++++++--------------
 src/builtin/obj/kernel.olean          | Bin 25032 -> 24965 bytes
 src/kernel/kernel.cpp                 |   6 ++--
 src/kernel/kernel.h                   |   1 -
 src/kernel/kernel_decls.cpp           |   5 ++--
 src/kernel/kernel_decls.h             |  14 ++++------
 src/kernel/type_checker.cpp           |   2 +-
 src/library/elaborator/elaborator.cpp |  12 +++-----
 8 files changed, 32 insertions(+), 46 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 688ead72c..eadd7f338 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -1,21 +1,14 @@
 import macros
 
-universe U   ≥ 1
-universe U' >= U + 1
+universe U ≥ 1
+definition TypeU  := (Type U)
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
 builtin true : Bool
 builtin false : Bool
 
-definition TypeU  := (Type U)
-definition TypeU' := (Type U')
-
-builtin eq {A : (Type U')} (a b : A) : Bool
-infix 50 = : eq
-
 definition not (a : Bool) := a → false
-
 notation 40 ¬ _ : not
 
 definition or (a b : Bool) := ¬ a → b
@@ -28,11 +21,14 @@ infixr 35 && : and
 infixr 35 /\ : and
 infixr 35 ∧  : and
 
+definition implies (a b : Bool) := a → b
+
+builtin eq {A : (Type U)} (a b : A) : Bool
+infix 50 = : eq
+
 definition neq {A : TypeU} (a b : A) := ¬ (a = b)
 infix 50 ≠ : neq
 
-definition implies (a b : Bool) := a → b
-
 definition iff (a b : Bool) := a = b
 infixr 25 <-> : iff
 infixr 25 ↔   : iff
@@ -52,25 +48,25 @@ theorem em (a : Bool) : a ∨ ¬ a
 
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
-axiom refl {A : TypeU'} (a : A) : a = a
+axiom refl {A : TypeU} (a : A) : a = a
 
-axiom subst {A : TypeU'} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
+axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a = b) : P b
 
 -- Function extensionality
-axiom funext {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
+axiom funext {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x = g x) : f = g
 
 -- Forall extensionality
 axiom allext {A : TypeU} {B C : A → Bool} (H : ∀ x : A, B x = C x) : (∀ x : A, B x) = (∀ x : A, C x)
 
 -- 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
+theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a = b) : P b
 := subst H1 H2
 
 -- We will mark not as opaque later
 theorem not_intro {a : Bool} (H : a → false) : ¬ a
 := H
 
-theorem eta {A : TypeU'} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
+theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
 := funext (λ x : A, refl (f x))
 
 theorem trivial : true
@@ -154,10 +150,10 @@ theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 theorem refute {a : Bool} (H : ¬ a → false) : a
 := or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1))
 
-theorem symm {A : TypeU'} {a b : A} (H : a = b) : b = a
+theorem symm {A : TypeU} {a b : A} (H : a = b) : b = a
 := subst (refl a) H
 
-theorem trans {A : TypeU'} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+theorem trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H1 H2
 
 infixl 100 ⋈ : trans
@@ -177,13 +173,13 @@ theorem eqt_elim {a : Bool} (H : a = true) : a
 theorem eqf_elim {a : Bool} (H : a = false) : ¬ a
 := not_intro (λ Ha : a, H ◂ Ha)
 
-theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
 := substp (fun h : (∀ x : A, B x), f a = h a) (refl (f a)) H
 
-theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
+theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
 := substp (fun x : A, f a = f x) (refl (f a)) H
 
-theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 := subst (congr2 f H2) (congr1 b H1)
 
 -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 319707dc5262c4149ca5765619d7bc342398c44a..958e9faac68707745cc9244aa12ca58393a1fe25 100644
GIT binary patch
literal 24965
zcmcIt3zS_|c|Padd+tmK6AOv~43PmQ1VKWgh|TIm0s<GMND?e>#+hV>j3zT-W)dC}
zYXvdL(^dhsJbWOiv?$987N7WnDnwB$NW~iQQKQyJ+dw4P|NFlEx@Yc8NY`rCV&~s`
z|NDRMf4|NRqiY8HM}~&i3})_6zJ6qQ!{FHXU{<_7%X4eBq8J#R$W{#wWyPr%ts8uO
z*5Nxir~_rOp?@qZju{<YW4&z72i6a-nHV0)Y7=AY2eVKc>R)5jNo~Z)Hj4hN&_E6=
zOZ=q*eI!;C8kL<qI?+EdJURlLytw~P{GH7&P}W6rbc`g?LLv>8Gg&W-0sNhnAbcR8
znbZ(aS1ajDF3D=vI+vt(tMEO0fjTj6&(?8UHr<i*QOo|3RY1&kFO4hyltB*30BP{2
z3&pHfdh_Oy+<}y1kBS@%&Q>SJ&2AmHWz+3RALSTcyKc?!;5d-m$<iW4S8&(h`PqqU
z*JXwMZGZB-l}#`Gv#4OVd}@e|VrfQ!i{OinhO<4Dl#}-d#r^1?Zh##G4*=LD%k%)A
z10Rtb$96y*{CTncSCwbW6}LKxgdxR;hEQv#v>2e1yv3kZ#lLvz5?XQ}if~ZH1zRqE
zw|YV2P_i4maCm%ToJK(7evRUkXa=;9l}zvwVzA**fQR{rxDYjO1~y8ziPh$cwSiuF
z5YYBS(V?LPNpJx`i?!y6!s|$O^<S73EBkE*LM;4gG>Yaz&4!Mm;9Rx7<{~wbYp0Km
z@<8~ahG88bG&VT2#*mky0g8%IM-QrVP)KM%!EHxbCC@Q>eEq;U5<qo$2$j@w-5_EU
zH^_>5Hw6{D-0F2S_M+&fH8`l(2h3t?ujlp$%!k&G3|`p6{TLIaA7e9SG*f5DTAU-$
zyr5B>mo)&LfFfaG(cKKVy;1!oz*~W0fg0oJCIxJwkL)OFmlyRIYYw9JuURumRE#^U
zQ5=iEv$-kz?#RAGXUZORv!QgNotCuJR(SreHN=`(3gJdKY08~adT04u*5PwmSLx#E
zc#F7&V3eI;&>})7Dn&2m+@w@gytj0s3<HbCQowjIAiEc1WOSl$cw}O1G`I=TK=LzC
z&LZ8j0cviY1CU)I_Rg{vDK$9JZ*-Od1%V5DXW25i9DkNa8=mTAq=Pu8l&AWDsO<Fy
zfXm3A0kr&J<_Zz*X8V~yAqo0p1FB{_d7}Fu;$vobe|Za>Yb}LDo){b6Fx<a}NQ*h|
zHv%U4#c)*r!1(&HRW0U`BM_c)#4L>H<Pd5qOPz;SX|)>QEXF3oGDPH{wL8<DZwc5>
z74yLWhPbH-Xnx>EeWm{!i9^P3iXfGl&(^hQ?VgX4GO$ronIH{Fh;p?GhxjooRTB3l
zTs2nFw!_uDeZ$+-3x?OjdIPq1SvhKJ<lqF7BORH!{MrL7CbTHQ;&zQPEtkr29vLsp
zyq7ujy=>Hm;3iP*0B`PY`UckwCz;&`cPFsAICuh}T(%xy=RB0}M{ykr5d_o)s>5s7
z^-YZRk6<lw>LlJ;3B1H@R|U5jB=jaQddd0%A`@iHN{WkO>%{=CBEp*m7EMQm(Zq=z
z@(beMPi%-ec>XR++5;}pC*7!$$!!$kuThtjZ;jyJMDT3@CGe#H@3w5^1g2T9N24qN
zs8#;ASc{k6WZyMQ-wk>np_G>cl$7s?;HC&(0T7~T{$3S@lvSgsm;;iRrU*Ij?bhr?
zMGnP(+@ncZMfjnl#$B?u36$<?kSrBsEm8bUbTHat3<uh6qxc&bp(tjkO6PZ>^&8S5
zO28!5r7iDOz;N3LpA)aO7Nw%KIzIrVO(NPmM6?nb)l)eC9fwfKcSrC&0QY7qy+12h
zySIn)b`S{KU@(n`?D)6V?9%kgQCp<?*Nu)7_lJI=jGKNV%C5Z)7#ScqOSuA6{Qd<H
zV=g%IMr(0Al<6lW3=zY!sJ!1r14P3zFqDsP27Ni<mI&SoP+s}~z^z)Cq>45cPoTXQ
zMXPiO1UUtPz&UM!fZd^svn2J{j&#7Czd&ej6cX!0043IkBX}FYZIT7fH|)-0b^nIJ
zzQGIEjb(Y%a4T#ohFg1p_=K52b;>O7-+`W9*_;8K%yTU)KxozPgVy4#pDLJ~Hd6&L
zKHG*u+mep~lwKc?;GF=snaFZnmn25x4r@%rrYIrUK57U~l(E6_(KQ<e7q&O^!i?L5
zJwZ|00Qyyl@)IZ|(I+E#w}JT{#(WXlvaKi<_<47iReS)BteU(TYaf0f(M36C1Ed?|
z?0-UCB78c6_W)E3-YbxM>%<z5MLUriRXf2;`6(NeNQp&tiYSzIC{?tMMEfi_OSI2L
z@bd=dJxT?L2a7`#%vWKW-e)Zp{?i0WPF<w#7eP!+zZAjy4a|FJz(1n3OZ*W8ZTWw}
znjQbqF*&J4e<h!A9#2k?R7TstuYkBj`6@uQeod`Dy=-OTein_<4<h27@n!2%R`9aG
z79mjjF_wD}0t%BDuJXl$#9`3>O9b75;$_jA;n_Z5c!6zoTNSvkBvYl!I8ms8GN;d7
zidoAfFXM<ED3wVb1}Hmij^MW<_-zC8CWU_l;E4pk3xplfr*;sMTawUjb^_@mIZ7QC
zyONe+Wv{z<qG|w#>wm992^le8MkoE$5b|X}Yx>Nh>JqfY9d!bETRvn6e*a+S{q^bY
z*h~^K5BCjZuV{W0lx3R749ZvP3<z>A8>Q>~;c7PF+|q@*9gtjg7H#!gG}1pICw<>q
z<mvH?)?)X(6gbIUgpW3OlwAk(;4f|*lc=RzxVG&_@JB#W)c-p`>GWfO2h2yg8ifJ_
zkotK@NzVV|NSpRjfsL($LeBW1wR;=;9s4wjC~$H4u`sJ>L+dDdV-LkpPi$nosD~Q=
z1hPr_Cjm<Np8}L}KLe;K`E!HvOE~No05{G@-)a;JLqI~MNrnSkMIDi77bRXFYg=p>
zuRTs~x#!(-<)-8)w<W{jW@NDMxp<t652iRM#4a{gBY+E@jPNVq%Lu>bP^$YI1M_Qr
zT;`*kXkD6&@M5|JC-LCpUs|8{u^kyq{$2F6jn6MJpD&Wnsg(Q&w%R<fvFh31p<hb<
z9-x%^13-E9zW~Zz|80=-?Ee6~shww)&l1mqtvuUdkfuck5>L)8breYU_U^`frn{X(
zlT+ZXL_d`#<s|ySd?SjR>9?m0bT)Vzplq-mplrakRW^9W8uPn2YzM&S7TwVXQ$_bS
zBNo&hJl~FCwl@j+6YG#6WZ4ZUB-Eb(GKc1XvKyGpc{W*$dRMeD#btQ2hkm%p8yai0
zvgF|TLsPK55d^tg%?p5HTLXBbw%%s}Hp%?fl-x5)L&JBn8-)-09Ab;H9gEHz!#;H>
z5Zc|j;dT{&P7TYhx5ybiXrIHmMjPpQK*7XT@~6%625=eeIgP-3xty{shmrCbKsc4)
zZUB1;&IEXd)~FRG=7p$d!=xS^swgXq)#%K%T1zhC=t`I(Qlb+=*3Tcp0B#q8alkjk
z1MRbDvVFp>x+Qh(TrBSofqk~a*(cxFgDRIaw^Km9m$EY?7}xpp&??LPSp@e0DARH0
zCEVwubq6i;0)sRMa;&y38Qz;I3LuM7d)i?|FaZx)`OiQim;hUVRui<ffb_NVydorA
zQ1yD7G|d!#E%f0-kFb!}48^5RSW4+iaTBD^mqmYLQ2sbAFxx<9xV<B|55T>NurEN~
zCFL&ysF0FFh_IhE=6@vkVt~)g2O6S?a^yb%L}uBUZ0xa8FJFAuk+d{u2V*pc<+1`1
zu0H9AMn$Wzz|pYy7YK6z3!#ysjNo!b{z5}*;FZKB48CUhoUs)2FnLcQaG1Y2cbjM?
zjzicbqO`eph<S_rbki?^X%gZpFb}}s!`Mn!C<`HmihbGI18|NK62s9Ju3|YxW#Po%
z&#EF3^E!W&Ln+wsJaqn)t$?r}#^3p)3{*<RIm6_k+2c*Kzu|=?Tz2s<5|a%hA;PwE
z0d-)^B$^)v*3$f?0Hyii05v5S09?TRhR;cw*UVQ-V2$hvS}Fzrg+9RxeW+o$^B}Ic
z^^zpv%xg+1aGzbt;14d%2JklG<VRbwqlF=pGkneyk(~5$bP42HKvUxt)>yo1zLoh9
zrRA)MWUANbRHKuaoJtY1TQ`F1z{X~nNjw3lI8MX~qBy=XnC=DH;zS!XkPf=WTJ?a!
zNwXMLqE{DIHnJOMk^$zU;&?{PZ^<rdMM_P`qzy3@;P_6oT_<NLfO&S-OjOK4D@Pm@
za=^uLD2_+*8WgD(k^rqIS2$9Pgkv}3?{$VM4He#rGUQh=2*)=urmaEP9dh|1Lvw*P
zJT&C4htT%wws)XD-XH>Ft#}o;(K+b&7y~5B_;AL7)p5ZV%Fn+L(3Cbyo}g)e(pU^I
ze>G?-OkvoJ`&6x{4$B`pS-r{RlSFjCzl6(=wV`oKHH8>Q_JBi-4N~MAQGOzNBnG^i
z9XZd6M2t@3>yE-C!n0{NFoWkLR%eKTOx@m6u!JNWv5mFcYc2(aX^zMFwIqk6kzWE-
zNqaIt<tc^`SCpKKfb!Hb>$kC30CKuOqeF1~rFHn!X;(q^(AKi^b!n*8T=^c9WltOG
zl?M40sLOJv5)78hv6m^XFw3Dm-(x;XOd(kY*3XYdHC`-q>o)BHv?j-SAjrJ#y6wwE
zi1zn4HpLZ@3B3yxSs*gu*{rx4BuIfdF0$aodT|}P)k8#_iOf>{<Kv?%Lpn|~_DZ0+
z7s^9}r5x{2Cr7)|HPrlU4j_0=1kWWHj9A><Km(Q8YJlBd$)3f{QZ<sMwA838j=^P5
zaT`bk0~EJKBQ?>}EA#^ab0KR+qC!9q#`gorng|S8h<OcDpt!@j6*pX;Xy4)vp!2#x
z=%mIO1CPmM(H)W#IK_Lsmbc8es-gz^<;{w$8bht4fRX?%qyz<T_HARLDV%dTh&1iH
z6~pvj_xM51`4z3Mi<Z&KLQ^o7s9UfHmqaP3fFcf5DDDF{J~ZPNHu*w;v}5d~7lDkD
zH)0?k0GXMJ2T90V>cMC!MoTPU@Enrm!wy*)Sw112vX~2UzJDjT)NSSJ6mw7=0hq}3
zh`L;yK2nj30|QgaRa`u+T%D<0$?bhrE{P=OR_0>>OR^6uY4NzV6_QZ-aXGLujpd#u
zU&|KnA$)^1jWM(h!3ZsA+|ZOFeQb7M`cPXu2{f*7{7j(u1?o42BIP)Zn)DUfisJ<!
zP*wBS)+T=ZIHll%rIAu{9HT-QPV}#zNIvC}Wr2VVqtomnfPA1Reh%;zNErEf04ceB
zSvl2866m?76CU9xjn=C-gNPOpE^{%Ma!#=AE<W-e-R*q}_)3ay$-p~HvancyWAV#4
z*W!A^B!>24`#hA-0#?c-AKvgVHkDD(Sj&NwG$I<I>l9Nr>P7{%Hop}#qE@xtQAfhU
z-?iN<e8|lAx-Ah!Wruo6z>Bgg%hGH*gHlR!Qfh6?drE7~FGH8y^7aT`PLTE+GO&gt
zYHhaH<%Q9($ab~8qHd^X%!agS&f}M~iG!-%&>&En14;#4l#cX#X9p6lH`LumqE(LC
zUPec0P!4X#H$fub7)Z5)yy=l1+E3OP2=1r?$=?aKNgy1Kx_5Q$@F*nh;sz>ACIv!F
zJvXJ&v`<!)CXP^8DlN8V$l6gRQB86wja>{GGmTa9xPmQV)=#rwL?bZ6YX8d3Rbqsr
zK@MAN{9QXb_*t`#1HFkdx519_N<#_9TY>US;}l_wsg?P=0ah|-4d;N`(dZ$|8uiym
z8R1&=#ne~*-j5P$HIGK%QCvp29-|W@a2*Op&^M3F+T0)|S!fp7R*a-ZXTm9rBpeuN
znBStc30!~Cz|=*JwZ^<J2%Eh>UD9fO=%_4Vp8BLf^wddM6Th_K`OQ;NADn`Edj|t~
z28ts|^@9NQpuUkHiX*-H?PC@wx1x~R9|lMtRn#6qM@4OXh=N}icrD}UK%o%!*KQHq
z6Ex@($$LBM%C>h9L<URvR;U!)*+41`t63hO3$@cceo9t5O87wx&1eoyG}#G}*Hnpc
zMpTJFaDMdYY~s(m{pe`@I1CN7@u&(8Iqu=(9{|cA{}{o$46Kb)%<F?L%+$3jm9IVm
z<e01D{Wi`4?zRGgr9VyycW;y=TFsq$IfD~leG(ib+T8@b+4NAMsEbsJD@c}9o{O)F
zCj)+sv0F8;XV>1<#p7}Kr4X+=9Bsirb_%IJeYpz&cSBseK9JKlNP3sL2UKK(dn5Q6
z18dh;+{0sV?M}Jp6F_d~o=;nI;vT!U+R0p^ShyU~LeUZHbd}aPZUH6cXMtLs&Kjgh
ziUhPdjdfa3Pi&R|+n7C~GP^}t<UrDUZqqDM(rOdxHTtqjiRvS(A*6BDw-aaH8|cZI
z+JS$GreWT^KZ0L2uy$|i%s5yZCLnxUe*I^RYv<Q5T65}G_sgfL@+7EiBOlHet`o|T
zUqzQ(`89%m8nl^po;uCN>(-3qSl?NyTou{Vo7MT_`L>Az$aQNRzVq~Gt0jI2wiCCd
z7NO-e2fs-(&}|Pz@L_=4Qn#VuD*LbY2l?tNXlUoFZ&-8UE53uanT0+x+(S({1(U@6
zEfANVz8%3w46NNV-^yYpTSE~-N!L%|nsPI6{k5)rU5a0Fg*)b@7@p<H;}>o{t3SVq
z^6{dQ?>-rKWyL<gwtFZAPcLdqfZncS1x@^2;N%3q2T<=r{|ay}Tfc8my+bNC(0mvQ
zl16`qqK=TL?}miqI2~+Y#v^bqvCc$2408Br3x@fQRs8)erv1?9nEfot{8TlH)K_u?
zh2>E}`*J{<bAlZ~`Tq?#Qt*cW4}&WCH2^94zM|yczTEEu(S3ydSD(W}cMi81E3|a$
zy#89YFw^iwRrz{B)D|+-_YV>wboH?c+3t_w3&@);kQX<imHl&k`jZ{}RH_=o1#Nxb
zXau_ylo9l;0OL}=-U8|}#ZLgr*H0Q$-?uumPDSe?&8)|P+-_$5*qW1>Rry_FjN{a0
zQBWGF2c#E5<^1OWCEhOpRz0;O`g{@k7m{o=nfhtXh2DB@g0;L&M7g~6!f({Njci?U
z^GmRhG)x0B)~|rDBsEsl2ZJ-*_0*fP+t1L@&Tju<%{~bz1FRnz8eOxh<?EGGINBb-
z`w94W-ug*Ydrxc3H%I1i(zAOu?aEo$#BeSV6mSV`{hw&mbIWf5O1s|y)Z+PjgX$;o
zXJ+~S25a_e;+~GGon9}%-@FxGNN5SC)(~0GK?^QuH80|ma{XM%PiIm#ez~Z;F-+n9
zz_ArQ^brE}z^MFD5a3l^{aiaE>es{dbHTjO6DYaIcTy3c4Vqx%zJnkcrdiTv=HO0;
z66MR>Y|58a<k2?{90Nx6)h5KqU`FK+2KhvJ3UxKGMo^rmXUIc=MXBm*0d^y-if03b
zRA6BK07w$jzrg(lBU(PAP#`S|c{BZzA_*k<00fzMWc`>qD!RId1EAABSa<3(V8nbo
z8Wl)?1gJoI2A~3Ihe7qr6d49Glh#i|;|wc!PsHfSH$(mU7#gF0^pp&A%_H2IaPrqr
zgOTg!pr`3Go*sFU*ryL@vR)vb2EC*!VyJ!v8bcr(nI=QJesvH<?vX3$#XnWtLwo3(
zC}EML_s`Q-Yv-To+(X+VHtHv#xC~}4P{_<h10c<;5abS?uP1(hE}iNpDa;Tf$?SFK
z3ey$M^~;0=K_??QHHy0RDazIi4o&zQ@ueJN0k+)KQEb^q|1QYTXWx;zXIQr?H{2<s
zn?_`c&}YltK&L5n$Y5QeZWP@ErCZfJ5&PKZVhq#Uo!-EQX*`7i^{WzAqp&bmJpJNt
zB(?puuf0TjI7sRe0G+J8cj9jnR6T-Hg6`uY%vn<GZd~hkvh{fYKS>bjy#5&<$Ck{U
z9Hp0Iz9DeeqKLdtY$7u%63kZr+|KY5!+`bI5%Jufi2j3UypPIr<|OE#oUH~rvS$4O
z6kmf9EgzOywV*F$H{!ZmYoPLn7;2Q8smVs`N%-F#`6uf6pxg~C6qR_oNF%c!EL!el
zR;q<uFt=*63C>1y^4lR9kRI6&UEJ^&b0hd-f`=6LR{;SWigth{(Paj9S&>7B+F}gI
zFGZvBnBoq*6uYX}HPMS(C^{mB;hP^tc@IEc@?uGIAW_RhtX}^~Xq`sdJq)RMg3_J^
z{HnCWcFW2GRB{y^?wM@5bBx^*uJS;$uOA;5H2d5S5%mcjr#{41ez!!?>>I!}W3x{r
z;E4J**e-tDqP1oRwMFuGDl#6WIP`R_FNq*?=~Eo`QfsY0jS+e)ZyHqGj>hdUnqK~}
z4)hIJ)ugMUCK9<+$9T={hy4mVP^4024l>e4WOU|mh|JwZ$d||+Y|6KjrEsmWG-HY~
zP<X#tHmWG0hv&3-xCw)`QY<DO26O)MprJX)t6>)wsfvbKyezk})BY=GVCgAdM$ig3
zaWH8~s*De*qN-om=I;eU!8hV~04h1{7sKi$f-W0wm5Z9%?h9RKqA06!;R3@+Pq|`U
z6FSOOVeJNi=JQ&aswdffOk(<S&$OI@@q2TAMNV9sSHSTj^n7tU7_@N+4azOzWQW@b
z`58I6d_Ky=Zm4F9^<48IzzWjnQAc_j%e@k#;86=(D+|`)54Xleee53xN||d<%eSNA
zQtMG2donk@oxVfpYubODTV>s#sip(EAZiIoWQ(YZ!j^}E$w7cYyZOlh>E)7Hpz|=Q
z_MyVmegFcMn>637$C-aR-?<r8MFCl8Qud-)jP9t8Ghchp03WMMc@zp{^YRGJj)M(k
zU^0!Di~RZr>BE=pAulHnRL?OlD^+9m)VC#hIHt4uHuP<W*u|@?a2fXK2riA_F%dl0
z!15FhI}YG78fyp$@ylu2B+b6~o~O@cyf^^n%pSA<$~ugapNG0_lbU@Jzqg$u7}8Vw
zcT%zh`A!g~-`dPt7mvgP!{}O<InaZpy<`+_ZpG1BH(jbd5krw!<nNi4>~a?B`cS25
z5YK`o_5tNy6;90bz$y1d@ghe0dkkcvc7mYR&p9F+J_aJG)<8foPcbdg{pTp4Y{tWX
zTZ4212LYXLCO0~_Je}Ma4T*DsdglLwTgjp_9p%kVu#_4!FY=mt=t#tKxfhD_c4jJU
znA&D@CYtiBHs($8{1|u~0-R_>CTR*&9**t>t$s`tSl2pGJ<}x4b3hI^x#b(I$d>q|
zvcxKrlS(+>#rNMS_j)~`7x#BGJS<t~k5h`*p<BB(UT_J-Ny4=*k07oY%1to4?G5dZ
z?c56ctAG{U+S3F?9(H-b3YQ#hTm9W~ak3!=t!%@+>pNHwc*<o*!ibd&J4=51Slq@m
zcN!X{(diL9BZAt=5Es!>*RJ$zg79E@O#{eCTyC)dqz^>dNL4%02z^^t-O39@%t(5H
zfHA{ud+}FRnPib&T04wDc}lWg=pV(<W*Q4dc>~qt#}qQj8?4n?M=5{^1F>}_`n6!d
z-{nW;Zp36(@`DO^xV!~*sn4+Bn_qb=T7$>WwaO&@b|s8$e7On5jg)e=flhYr!==$1
zW9yqDxCW?c*ghpaVDrgg3*>9j5oE{O7G&2Ki1y3IT{>`q!qZ8(KCN(NIUCHV1gx3w
zL;Xh4D5cg#@calOJvoGNgX&Ln*aX4(R;JO17%q;mf^5puSzm}c!dL#Ai9zKxXoM`9
zwfbtCfsRFk-%s_8*vS!VKEt@UouDpYc;QG*xCKS{7>lYjXe1Kn&P-JOkNb-et4uca
zF3kg2Sz!pd!xqZm5?QVMIt|6UE7|uVYju{qID&7E;3eq)5r@46Aoooz_DxQNoEQ0A
zjFw410dP2`5ja^#0_u-{zs5`|iJz$&lPEMMXQ=%5J-;|yV3a0X>;E*X9-w-cLN;0D
zvIxFCf|p0|9Y9TIm0JwpLg!$rN)`NKpq&n5DNL`o8G6vdy{_4su*zOy$A$;&U!TBC
zTS}^Sx5?RntEA18C7auW9<6Ww+ECGmjhNOQz2&iPuQqhO>!8+G0#TQNR{@j(t_C=F
zo)x^yZPe&OtepCwYQU{;jT!=6*B4Z5Yed}YxzQ4Q56h8Fm@TDAH{`GU6r?fJXpg9$
z_cQ#ZLxWQ#yel;!ntqTY>Y&R-1;5uurD6X9m6X+Pd<czjM`LCb@iD9GSIQX1q@Z8_
zRenv8KWyELK%p^{BEvo!NM@USP`(rG{AVQF`7%Br7rX4s1>hci+o+??M~&ir0C_22
zydR)k`1b(k&bK1&q8pfE4fwrrP`jQQyJ6e<K~|WjP;#FD?=}vo)C+H83Z`%1B`6=N
z3z);GpkVCiDeDPeZ`8fr-fK-QcEd^&CqX&~T<F_V<mOEvl+C56hx%xfjkvBbAQb<s
z;~BY8hYrQ9R=BYL06;xqd=Ov~_D3;PI#|8{eWx-<F&4R1==9Nc6pW_N-TQ%P6U0Sd
zkJa>X=@N8Erj}lP`rOjXsA{}2phfCJLtR8qH%OC17AEGOz^U5fZH*m^Z0+8oTWvjk
z!jY{}wtuAqWBNNWJ8!@oI{G)z10MsZ#Pe~0irPB?CLX}5)xaGV+8fIbwo=b*Ar<J&
zhW=%?)i3Z_hah!2%T|#KK!K-pLXFd-P5DG40qwvqzj2X1EjkYZXvXsbPfvqDYGCiI
ze~(0tOfbFND-yX4xxQO8AXCyA;1j=qpGxLz1!Q)tVMI+$y)#i`NsS&o#61g80=25r
zz&2l=3Tx3vt!0|Ph}o;%O7vU;BgtWqwy_*CD2LqxP|<KNKt;o609JF@25W0z8Z|DM
zZ)K9**rSNiL*jR=Us^WS8_=+S&{y7NlBg|4Z<?=Q0cVw%uY`trW4WJ0pSD_ysan?T
z=aQ~s1laZ<5la8Mb&|QTa`P><!GF)A_?*?9r9KZ(nd=JxlX-*8+qlxl-#e4|^V~FV
zxGzvnp$Exrh7F!71{>GW=tG9${*e!ji~6)oq5M$@!eGNr?gFl{`9q9%{??Dvj>p3~
z|E&T>x2xMw7ovfB@(BbacoZ}j0WW`;G_N+Wfz_nJPh=yt#*M&YYJwoBG_DM)@cF;a
zD=y^$PRn-z3)qypJ|kKY<Lmt9Sm?Z^FYX7v-g{}+(@>{zL;h((U^Hi^g}IzOEVw&w
zdSSI8(R?nsTxa#VL_*I)Mv0o&XC`ua?@~dqZrpA~o6iceB?*7vG4{KH5$RmV&PV-c
r4KL4Mx6b|-2JY)BRqPA7Optx?Ex^_k2MxQgQS;+QRvnN3^}_!Gq~<w{

literal 25032
zcmcIt36!2ydH%ldUr3mQFtOmlkoYNN0S!9Af*vB7ur)A15t-x^qvK3614AY=VKNDe
zh{Oehf~?jGSPkHU;8NErD2jU#5m2lxh{nAx(Ymz_guc)7-0lD7&xG`x<{WO```-7y
z_ucM$x9<;QBZK{;L&GD3nfsG(8Xev|IKFW(D|)j$H>?%Kz}Q5VG%O4)?6tXnJS&bH
z8ym^?K?mzHuxWT?Vt6#GO^k0E%tCFbf5aHC9URJvvo6{&*lYA00ey;nSjNVMzEwQc
z-VD43&(BU?zacB^Z~K$yr;knaPYjQZvR1q_L$4(To5^$3RA?6cSs_V5mQ8P<+?OEQ
zI8sqa%&e8;y?25vTU3x*N{o$@r7%|ROMd&a-Y5p}cQzf24*@hQ=-S!J`jShsnzhd(
z>sgg?SHD1w;Ba7TzwKK;khD?D{?WA{%=T~CsQ5EI$RQaZ4gPeZnBB^6!2+^7gmN5M
zk>drc)rfv`TKjF^`u?O%);6~^i{%+v)q|Bfn$9X5Ugn<%jtA3n&j#2*umspCndbwZ
z2J4X>`*y(j_%ql3t9pO?74LEW7X?KcUcX^vcyJ>y?ab3+m`?Q=8rmJTL_+Iy6cVY`
zDoYn1ORF42p%+xlx&87R)QawlIo#ld!y6|y(riE;+$_$Bh69E}$!O0f1ueB0;1S-t
z7oz43N2Fw%IM=4i`oM4cp&&aDMTfc)B*QL%7B?$K6)H!wssF;PSkrIQ7h>VhzRhAq
zmm<5PC^*rrZN(CyIO+^<)ai%7do^_H0Hg82p%Ei?@zDrkbws;LZ1(W3eu>rc9Q`+L
z8rX>Gyd3S>iGG+EUa9R$(AYE#(xP5cR1F8&>Od|-QPLhIz-4~qrB<ou_6LIxZ5kcC
zux0e)q5|k<@(dZqxdNE3W^qo|1avZrWC#;^MW9_4)$az~N)%l}#@;;?um^1&C`uHa
zUept;5=8AE8A(O8kU9>;*%8g+cmi|N;mbHYLoFR1)Mi8JL_2l2)K>cOPcy=rSqcG1
zH))!_yiqu3`OMVeGgD{7Mbya_a}2)h6oZyfz*CiQmu7HM11KuKtl>l%0je8?0>+Ec
zYZx!a=-5Qx@aV+&Sa1`f0e!NWC}xxIs{m?t^#Np4NHecAjFcLj=r=x285lG~A9|UI
zl{9*zF;{tEOHfclCAogoPvqzW052lQ4BoqtX#?Ig4->zdAPPF>VnAj@xuiUl^q3+(
zZoDa8ZJ0u`PmB+59`2{jvZaTDbPEc4dnr8DKd^Dr_}ZY7W(`OXr}D^bRA*44VSqB(
zc>tx=I)Jkoq>RrHn&%qc+3<YJ-rjCD2(@=}6ul1*qm`&i|MdVh8drINW56CxaTsak
zA|NOO)zX}f1|*VlwF(ELn3XCy{1PrXYiZk&Y6^eH>(z<@Z-n&*Y!9?%%+{H~3FJw-
zH*=|WKB%Ulh!QMqhm>h2NV$LmADMYCv+KKvJO>2XHWVEgo12!t!I9x4$@?gu0jf^g
z-~xcM90O;@0wCUv;sz9A2&fZWhu3fDn;7pO#j@noNxZcNbcx%p32rk;<UOER#-SOo
z8u~TtN9-jLd@aChh`m%`vBGg-G;xN9M01gm_!$l{2hZPYN#|pf=#vsv4stt%cs=S8
z_ze+!V+7v>Py$~L@KctyoWL~ejX=r*fLi6>Vi+&K$-Z}%{uKCqkWyX&P*T1nf^UuB
zl>i}{=I=F8NLe+C%EUl<OY{lJZ>v?js7R*xj~hHGs|a6AZnMx)I|fR34eHYsWGzwr
zZ8U5P1!FkyZX3l9fLKv{JwWNqsC_^>L<yLrI<=F%8pM_5;X1=86|L8?03>Y^(ZUeX
zN@!G1;r#dPLM7i3!G8d_kl1$uoE@yaY(D4hxxi|t!89JS<J%4G()5}!Tdn#xjA^s_
zBfnzCy}U6cn}r694iKEJTmdeABLj#r7aVz$VcZzX^pg^Xn8m!`NdrW~mSC!UOy|i7
zw*V{fR)F%-Z2)&@VcHBh(+*=hK<4FE>E2^#IR$~hIc<S}jiQUQB=y+lbU-^zx?~|(
zO04$*lq~O$;0FNilq_(*QBNz*?cY4uH+bQO@hp!T?to1-;Ewqq+-@dNoifY&cc5jN
zZ2lg=$vp2sm8!Ms_g+Ig>!%7PhsabxFv)hJ(Ej8@0HxQ5Blr=3J56Lcu2T{lF3$~_
zh%I?ecBiI0jlzjCKDcpgWb<HGdoy=s+$J1|VWbV9-!Z^H4p0((B7&bZFh9TsSGw7O
zmM%Z;$E@N5aCGhDU0M6^1B*_|F$Z9>r2jMO65%ru{47Al;9UZ3zW69&@5h3jl0ZDg
zOZjQ*lt_t1bvIEc>rkp_9mU~27+IoyA%b5tFh5MG0P$dPh+;O1Fik&imCE>21WA4v
zI!oOz0o0&hj^I}e%nzdhp8~d1<0A;#j(@MA-S}hUa#D-_N<QJVl^iBZaMU*NYXBw6
z*CX~D!upN=4kYfp0Fr*85ld8qF}`XQWd$z_Y!L!QA&!KFUM@^xxXKsbM3ZE>KZ4%^
zXr~W%=%5cmI=;`^!m!nCRTzB@ShyWfoG2xb%A74xSDKVZqAkx+Dw8}2P_jJ~!G|OG
z9Ru@IIpe+y@HB$o1DHpj+KEUONJ6`38o1of!E|cuOfVzLULVWQ-UKDr|7DIOWW>A|
zPRf31|K+`adVFS4wHr9*ylUa+6V`gaf3TzfrgV1<$9W@h-!KF06wUt*P^Nj*p!^&i
z2Dx=mHj>Y@&c6`Ui9a<VqkCzqKZ2%25pvSMSw)`Sc+q<7o|mJ!{jGvb{G9n9pq-Ma
zrCWZ)t^~IO)Li&6K<V@ofX`WkavcgXC;_RRr@Z7Mpa)Gf>@q5_1@+h|Op_lP+S}Og
z*r!lLfs26b$|~BF#>qu*Y@rxxiActaTBz~Q&{OBxp97TgzW^xZ5JPU6{ttul%h>H#
z0JlVwC=4ShO)?UORn(D)c9EZbto_vb@&4oVmJ8wSZ{3<4<$jvsa5FmC*Wz(IyZ2*M
z9CkIsF^6RyPJt4Q8jjKsS&e|-f=Kt7T>E5%-?1yz{k?(t^*%21jhtwmnv6dLnYI!o
zATkd={*7V0kL}1{^0#`rtpcg1t$%)*>9izKs_I!PRrM^Vjg<Nm<dRZ<1}M+|1z<`2
z{>vce+5ZN(t(|9kNSb&S!^*RCsuU-Z`{*c;?CstC2kS<6JBKExKt=x^ZBp@MX$)QT
z8<1nV<+o7SooJB_o&YEtJPA-X*ac8Fc*>ys<LH(H`81<D+F*Cl{XfPms5^MR9mCol
zm2SeI6iRC=b7)=z_9pt5C)1^*iZ-6kItsSX58Irfxne0x4xT@>n_+K8U+z|OT1>+>
zfxTH<Z(O56GQTzLjM9{7nSr8ZLg#hEXka@QoimPosyu7gtjB>oJ1g9|;hGhHR{5E{
z3=<fCR@2SXIM*2QdRtI15nF;xHlrb!$8tUnokd5|9=!x9<|=|S(Tyv4z8}EVTBCYR
zOkS{LBjg?($|1`}aW1HHt=5u@G`bt6h$Sda30XgX5FNNj@EIYWW~dMkw9k^s_6hgn
zmd=#dN@uY=clOD*$UYd+?GykmqwMqt<2vVhE6Y3s1OopGpiFlFK+$3oW~UI8&qTot
zpL0#8rrr?FOi=(?th7GLge!vySkJL^g#BR-=~_+D)&fK5l-YS+5fUz_EJ9?H9y5hs
z3w`)d&P3RlI$?OFs}g*5?h-Qk8ye=1(*n-|m8>-<f(HZSZ9zU4An%g$c>ons&j!d`
znU@CTPm$Sk4J@)nR&ozPIr1N%or7ho0lEul<ez;YlB8u|budP0xvW4~t4$8Esy2d-
z3Q8Fj1}0;6U?H*?s($aBA7rFWJeRnH!G|rMGc<WEEuR67c#6<0)}4dW#PirxqO5GA
z{e135n~NZWv=L@<&KXEY&```S%0df`s+dPC3|F`db8P+)u*I1K!im41RYf9h81hHi
z_4z=LkS+JakD`wKF#gUTWuQ_j<uG71dwd#&C&CggyZEPx$%c^-+=PHr7uXjJltl9v
zph=o@2Q1CIfYp>-0<g<uMC#OJ)4YaWSvSqKok1G|fI|E8aDIf*x$_{dxb>tY;acv@
z>`DfIaA`JxM-nGLaLJCA*)>t%D74E-JOBuMF|e8%FEOY%9$w4OqqGdk$fkOYPTn&}
zxevHR%2FqVjlkLrvsGvUP;s)D6GU-Jr88q3Y>U&Z(?HtkI>TxN=82`KlAKFh&dm!2
zAd=1YXtQE~`KVBK|6@ffa_WIh$wLPF&j9WQIg3+;>$01$iaBWIm{+y3zQyS%QY{#>
z*xwarRz{>4$%rN6@8w1+4Lbl~E%(ZByoy2CfA<Dqb6C#)+8DY(8y*^R*F(UqXnP0h
z;|(G(){5h~jn2Wxrw2f?jGu$c4dX_^7Rt}R5YQ{oB}?9-=|A#V+OU@VZ_utVC2a>1
zLUA6jj>_LDu)59U<0RC+Dx}Gij6QCub|c2omDnIhz7gf8VnB&;8o;9~V$85{yU^g4
zr|kes6v1;6Yet9x*X%6?ze&PT+gQ83Cd|i&P8qEAu!IiRligx~msz35!u(|bm8Z@G
z$Q31LG$~J=Wk~B=;4cP@dWYb^df`*2T?N@gTgy|Ia?kWubL9t67TyOrrNMrs70z<2
z2nNgL*uWH5ndN}b4`4{svn3F)etrTVOkx?g)NR^*z@{hj;B|N1_Ei#;C@G4+u_>;K
zgMdGMAm_$GxWOo{_08^J7=|dJc5wrmnf*9Gi8GN|s(<6gu{9wbrx|+<I=C0g#lcc;
z>`<3L2Q-W{?_&pouZ|!ifv-HA1;s5*w9Q6=GqBxW$)3e6QZ=%sv?T~TW1q*YTHFp~
zFhFs8G*S;*mWiCHkPBH)WGVvRUt!u4Ei}RwD~dZ!F2xPkC)&5T6V1GCkU`0f28G9D
zvgi)U37X=aUdvmftk5q%wIZwfl-5KAC7>jL3n@YIQ8e4eL{XNX+RD>DU_pC)m6F(U
zenqPrqGhPMOu<;9ZowX05~ZL5iZtL^+=J2hNQYb4<O>1vj<J(o1Tsq2qhk^p_mh#g
z)csK_hJGwy@Eo1<^^RB>Sw0~heZpsIlZo%&$t`tTxn^i^a6KPjBG)5oa&h`dMJ{#>
zgHo>I(kbPd;U*vDN^b9~a!Di&Ze_j+;B*du9YHIK$5BW^<;Pw$>9pLzJx#uW81Er`
zjx~ibv<*QIEoc`2oG#WUWrw5>wZ$*c#ubjA2^7CZeOoBf5vNd-zT&VN@nSHjs`-1v
zX*_<MQgFdiPbs+>y+RmH^lzF-zUh%=LBPGE#<>J_K2Q|DViOWZz78NIw+|+Fw~_>Y
z?&*Z*HcF%Q>QXS#^7}f13#?@R<BLqO%f&~2nC|vI4I+0O(2{X4F=aq^2>tmg+Rv6<
z7@=06xkSM%RI3q0QKI0!rG~lZ#v&5Y2witGb)#-nP;2uW&@)bv+WzF^gsJV1gqn<_
z*%9VM6qOBO?nJZi&9XFy&Y+Yfq!7DSWPTVE&YRILw``5z6$FEaYB-PA=6GG66{SVC
zs~r?|LtXFI)K%wn4Iev|AWFQUPKK*7kJ3eHPe1OQz{0hLy4y&!%2C6?I(2Y~dS%>{
zh@l}OBdjg*QGoQ&ezL|ua7PvEmtSQ?8VKAqVrd4xwj>HkySR>ORpwC4CavhWEtRHy
zvZ6HNhaL*cYXMeLN9`EH)g+hF*lR)ME;5xot|TVR`Y9HSXar_w?Y6H+_hdGlfI7C=
z_`7xjjS#1z(z<KS+y*<wD@`F9Z-prq3d$pD4Qgfn4uDlN;B;4$WEiY=EQr)oM&O!~
z%)!d{ew0wFc{IY&WYVzG9cK}xOmsDFq=OMw!U!3&wt^CUG*@Q>Qfi7u5^`!Ii3Ua*
z=C^2V0@q(OFm*9nl>6U>G3l}F-RY86TZ4wm66U#23PjJHjOjOpA^W%EKD-<5?Hvr_
znJA8?f!_;I59(V8qBz>C-#%tRavKV%{eFP$1RF;~MQwbDf*%cdE#v7xp>PQLV1Mlv
z!2?mJPbBXLQCGITgCJrfF?WSav5N?DVOY)f^cSI@(>#7kRy#)YK@81kc1<+d1C!IM
zOgJN|OfWuolg=joyxWh4){n!0s9g|M!6C;zd~n+?gZvY)0zYO@?E;E<W6*_}x^}hl
z6^}bvi7pB<e+K`EVccy61WSK&;;*h1FVSl5)XN#1`05j2E_psl(3?${f>kcXRaB5%
zo{q1IUj+Kv7Vxhc*bmp<)y3nnJJ;}Pcd!ipu^oT)>1zN4{1yX$*KQ2#cm{Ru`7CKT
z)$WSm-Rw|t50AmMkIFqC2XQ<1e8$j;d+ge34|9oPEe1FFIo9baB^Pc1<*Iu?TAj}7
zq)3Vkv^kA+T2N1HmH^wBJ(6mX4Rtw?{I+3y7VZ$R2TodTA}9K?$_YG!FLBkk2WQ?L
z_{o{tfqxlnWTme}@T&&a?oOQ<JC`7X-D}^KUq1&#JHLL((5YYDuZMP*C&6VW$KiaT
zYn36tjwT8D4T63ew3&6DJI%%G){N{}-&3kQHx5s4R_Bi&w@n;CuG?bwJ*P)oE%9Tj
zJ-98kNQp7@Hv9lUS>)Rhd=TKy)NMdqWB=9uB42$Ch<3jEmZ1}0@g20yEOc*2wYy?G
zB#HZBFqc%{iQsn)tlhQ9%3>C=p(p{-&uj?Sln)u&34=S+c5giO<nileV3W1}4kyaT
z{T1JRGVaRU>yO{f@SM>N@^%d?ndZI+{&j-?3Q+Gu-v>CCSUiE%JEUS0Xgv4m{4pI6
ziaJ7~z8?~f8)>0|+3Qg7rIJsBv6G`mb1=*!R`K_@SjmRQ#_jh>=BMQ#%c4=Fepn{6
z-l(9xHfY+=@JlHF<LpiFhX9X&D*1H)Df&Ed@^4@6M}=r!V*k~3eXDo%4EHMa`8uzk
z1`@rYNjr|&g@IzderS*gp&Q?O>eQl(W7F>P;uiF#SiGH$cJNcFY77^&^?A_<b}1+$
z=vx7XpM3pOaF?%t22j5KIgs<JGiw#FM`>pL0L1NP)=vzb%&f{!6x+Kj3JQbO4+HBX
z=^j4ZOT1qJTlLg&(dRE>FWNAgOzpJhk=PQ$dTxTXyiG*8y!DRr-Y<=B{Y8}KHyA?F
z{1%{$g^W-?E;Uxvrv%w$_Fw%}+3lA=w6oi<4egVFGQg(Mp|O#*@#~fJ0lc4V{5x;`
z462Pia{h1}+%BKxb$tgoXFfVn&K^KoG5~c`yZ;1uFu^|nly-jvsKxV72G!5t&&>4o
zJ7=#Z?rM<P0sjL0&0FCvLfxEN=W*z1z>J{ayogWA^#RFGXHqswth_NoiT=#KB#V0J
zBLwP!UiqV7z^l6YfSnQT2PgKYK7hdsJ%Muc_)aPYCCGX(3}<QHOE#F;?%9h_uxsAy
z?3y#pWKo`iqOia~^$`<dbTFgxw0ojFg}N40<0#hY8Ip;VQq?JZiEgzba7YEV7JkCv
zg!H@r-y6PNAjQvob`wbQf%Q&58;F^sVtZw7>e`7uSa<3(VZ{7N)D=j(04k840?0t(
zb!2_3BEyh57Sj4FQ1DzEo^bMqp?-a{6^VcJlzcXjB?^!uFB=OiF?G(39v}O9<cU5~
z08(zQg=Yu9l5hPga0-EJY*sL&>(>TR<ev4Qa~Ek9_s|~tCMr5SENV|!zjpo!%UT=v
z(DsY1WBm*iTVdvc(}`v-usq1j#l8T!gXevV@1RSk`WXr{#E2Gb&R%z}FkOMJZxs;)
zolNAyjQ_ZT9(qRxhbH`u_;U6!4bBX^DSPd8*$QoCvvAL_N==r+w7cZBXGWcru1b*8
zlpR!`b;X-;bPtqnRr5^j)2xfpE#rfgxQ(#4!k`CjC5nWxkfMrBKK&a@320w?i8mkm
z$lE0VI$3+~#NTA7dIUK(4{XJL7)$QMdR+e~ojM!fCkY+^@N+(nEtxwx8eR@gpzDlE
z5qXb>iGxwc(%P9J>R;RwJxOI4>r=lE5zp<3_}>rYJ&bkEoP->l<A-JSZ-Vk)poB}P
z>;&Hy^rh^kT$Zqc<U-2L)MSfC);a#C;`oVrJ}75m2t_5HF4D+U493eUi$f!}ofSvH
z+^Qu{2FY)SN>IsV1i9fao&&7F=Mp>&S*?Ho4zC^G^hPuTo2=ktPwiNA$S(&n4N2@$
z?5bk#L@#co7T5qVvh!mws+J82312#SxeuR?O;#QIJYlDh7I9c?r?jsEeN|dJ+1d2B
z4{ek8fpE_h%-k&2va@+$MPENYE?Cj$eu%guga`Mz%I}saR`d<vnsG&+JXKo%`p#C`
z91Dy-87&S6e`))?2tGf8aIz!7I$M8&MtUK@CpkCH0|C-OaR-pQ!ghim?DY+xIpgjj
zPe>DqT&iOb=e<7hfg{;A8kS<6He!R>iwh`5XVGDmBIHZt4x;j1Vdm064c|d)8IJCa
zeXAsf<jrS;=d^gZ37yGWm!nJ3Ies{%Ik*(oabc0FXvpHI+{$V8Ut?yIb%Iv7UsG)X
zh()Qv>BWasan&zu^P53X@Omg7fEv(0TMDZ;5Omo{t6UV;c3)^(jUxSYhjP5wkWTta
zT@yOWRT<iKvhIy%v<|A4xI3IY=+S=A24;Wb;E=Xt0WQcZ;rLO;ad8I*XyXvQy1?s`
z9d1Z@6G7g1CT4SDHz3V!oTBdotRRgZb*!hb+%f1i!~V0dwX$Fx{%~ttwA|sXgDVF4
zTvfc;=-vK``f|cJeUk}eL=6VdZl(j;89XqZY!Ova*z!;?IS9~mKR@jty<CDtmB;l4
ze*U~$KY$*loXY%D`OeL#Dhb#^lg4rs$D%o^<ILCIGoa^efHxYjd*el{KhHo0W&=5`
zag<;GnAH78)FCe?4^&SxFDq3eu<JXMJlt;xi!Gv2?1I?(7+ZPwc&ob%dqM<HjNnNI
zHu&R+Vg<ln8jG<JznrE`((H?KRG$WCN>KLY&fzg|;g2Embr{CBNh|s!{<3zCKu}EK
z-$}_5>@h7e=Eyd)*2N>~T3zch2U@UIX)p>OZl$3y^$IsRnmG|qMOP#i`FmC+yY!*1
z4^`k7?(`bi2Q&_<jD%%^!!_oi`Pr3e%-&o|202G$!^hg$aEfUO&M!p)WiuZBW2`3z
znGYID@GwWCa~rEU8lxd`E=XVX|KL_kN4YhMC~v~yP7RtDc}*>JB!l=M(5%~&srrnn
zZMZSfH2T_@H_7uj_%;?-{0QMFOk)X}k8Jg0qQFFJN3~3mIN^f^c0&#NzS}1i*eU#6
zCL|Txn9*r1&zxM~fKl}Ly&k;H?Sl4q^erq|=Z{nLLkcC3mxEH^SrOz_jIb*W+qe>D
zx4ohLv7H;1y#krftv!rnj)89>f#!BDD*^grc=0l;1g&htz4tp<FnGdcN5Y7e3<;Uv
zJ{Gq#JMx}Fvg3xsDW~lV30@ho*j~F`DFUbd1U%Tdt_cbzp^*UfL?l&ZGxT+vYOT7J
z7l=3k`9QCK6)ITd?~M5*i|p0fVGJ7f)4H&4*FTD(&Gb$*-b9VLEs#kVFaqgLfrC&}
z;1GGT+c^L~BzGewv&Jnb;qJz*fTX@c50|oy+kg%FAzUZvw>M!7mRF*<newbN&`C+Z
zNZ|DmI~u_;16#uO3F!fwPYzoUUyp_$J91)>U0)#X?STs%o=n2^NrfxRIT(yez?wN<
zd5Uo$rPRg<PDF511d*xgPtq*7F4K7`jXs2HaU?omn8s?>d1a6AmH%cb+&z(It-jix
z0c42+pAPkn+R5<{)NpfB+(EFUCQkuNP3#WOpS8FXNTmrxoI79=e%xQ2Z<WcW-m7^4
zE3XApUA*`$l+_zZWsUo2sMml%_Pr#6uZ`fP5qzD2jUThy7J%G0r5gEcOzUD^<j+NK
zne-C?M`FfchNMZUKmPq1Gbts`W!J=*B%v`eft>%o?-vJLiA}cF|7lizlj>cLF=Q1U
zCj@Sd*efFV76V&mm0JwpLKg*8l`8nffC)pf6sFgkj67(eS4R76rf;qN^P1zs1NN^^
z;A&$zx!T?41_HLYJwRczx$}XThQg5UN|MotjhKegTOR9n<>_e9%Gbf-Z2%9Z0j>rp
zt*-$%cYzhW%WdvM7jkRG0y{O3H21;G(XO}zVn-z0;YXt-x-nJqb)bPgq=~-VzX3=&
z+koaQYaUfQ?`QZ+hbE^=cvtFyX!%*_DDHr;Li0CX_`7NU0+p22ZanPmnzN#a*u(2J
z6+aE@LO=cbukve({2^<`rpKg%$tjXLa`-EKP+nz?x&>_K%lLq7PTfmiQaDWx__9f-
z>rvxfR=04p|B8PEBp1FL;9R=rI%2J8E<}M7ZgWw)mVMX^+t$%+o<hkjLuo*BL8adG
zHl|?u23~^l>+k~RaADX9h<C6eL%li8+wEqnwb%_SO`HVj9B`p;zr}rED|lve8SsmJ
zw8=(XR~QhAf7VwSb#odG#bsMze;b(arKor>z$EOCVW`YtiEVebD&+ob5Ou5x_`7)w
zjHXYAnaym1xagaY28@|?qmWFktu-`sqwuX_x-^hQ?jmEIOkZKWG&y8pwvb`9#oL-W
zn*Zjhdyj6l_0$PRwnnKpQk%<Z+M$_CYt>7hz6jzCm?KBi#Spys5I}k0!vGbv9|4$n
z0IOEh{!vmHq!;n4XSR?E^k&0>nM3po{2)l3iNjVA><)BFC)8XWZOSJa|K{uT;YxmX
zbROopW;`$O^fU;fW*_(_AGRlyUhY+i+(umAFB%XsH($wd=(Q5<yOB9t37Or{^ggGi
z-kGSeq&6Zw#3>*pP^&7<SA(cT5!RwRt)fZTHZWrLYPS+Soxo6PASI-2GTN2HJ_|_{
z4R--lG~5lan!~X0H#wDGv&g`BGty*>B1R91kDx!bY+htQ^Q@L=)feXyO8E*Fn3S(X
z#(d@fLC@kdM%H4gmNon7q^lSKl__)}L{J`}rBLTvYLnm16kkBQEcHcz%3SvXOy&)i
z_2$(+{@#|vpErT#4M*!nXU!XqHq)xRi^1j%G&+`3_m6x?%BYXsnJFb881qN1P_SVq
zcLA-PKZsx~_**|tJ01_~>qB(Ax)He$4cwDYAgs~;r32&1g*ktSJg+ru6ANPV##U}k
zEHRFoH_O#Q6+ZvhdBvqXz-jq*bb;8Ex;`^n5mTzpZ;nOITl(TFpx1jZ?Rqxq-6%r-
z>4Ct&WM?PxHGsfec6Z+NLNK3_3%4Y7i3G|AjT1Gm&r0O-wugWmx_JknHsg0E;~Pbj
z`Iu=;yPF3M>4x(w$32G1^S|9-|7QaCb(JdiZBr)5zW5ekYl?%0-Pfr3iKA;z!vDSD
Fe*wJkM<@UQ

diff --git a/src/kernel/kernel.cpp b/src/kernel/kernel.cpp
index cabbb071a..a35e6b391 100644
--- a/src/kernel/kernel.cpp
+++ b/src/kernel/kernel.cpp
@@ -16,8 +16,6 @@ namespace lean {
 // Bultin universe variables m and u
 static level u_lvl(name("U"));
 expr const TypeU = Type(u_lvl);
-static level up_lvl(name("U'"));
-expr const TypeUp = Type(up_lvl);
 // =======================================
 
 // =======================================
@@ -92,8 +90,8 @@ class eq_fn_value : public value {
     expr m_type;
     static expr mk_type() {
         expr A    = Const("A");
-        // Pi (A: TypeUp), A -> A -> Bool
-        return Pi({A, TypeUp}, (A >> (A >> Bool)));
+        // Pi (A: TypeU), A -> A -> Bool
+        return Pi({A, TypeU}, (A >> (A >> Bool)));
     }
 public:
     eq_fn_value():m_type(mk_type()) {}
diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h
index fe9dba7c3..777fb8a1b 100644
--- a/src/kernel/kernel.h
+++ b/src/kernel/kernel.h
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
 extern expr const TypeU;
-extern expr const TypeUp;
 
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();
diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 225c577a1..9ef13bc9d 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -6,14 +6,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 #include "kernel/environment.h"
 #include "kernel/decl_macros.h"
 namespace lean {
-MK_CONSTANT(Bool, name("Bool"));
 MK_CONSTANT(TypeU, name("TypeU"));
-MK_CONSTANT(TypeU_, name("TypeU_"));
+MK_CONSTANT(Bool, name("Bool"));
 MK_CONSTANT(not_fn, name("not"));
 MK_CONSTANT(or_fn, name("or"));
 MK_CONSTANT(and_fn, name("and"));
-MK_CONSTANT(neq_fn, name("neq"));
 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(em_fn, name("em"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 034acbbd8..d8d0fc003 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -5,12 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 // Automatically generated file, DO NOT EDIT
 #include "kernel/expr.h"
 namespace lean {
-expr mk_Bool();
-bool is_Bool(expr const & e);
 expr mk_TypeU();
 bool is_TypeU(expr const & e);
-expr mk_TypeU_();
-bool is_TypeU_(expr const & e);
+expr mk_Bool();
+bool is_Bool(expr const & e);
 expr mk_not_fn();
 bool is_not_fn(expr const & e);
 inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); }
@@ -23,14 +21,14 @@ expr mk_and_fn();
 bool is_and_fn(expr const & e);
 inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); }
 inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); }
-expr mk_neq_fn();
-bool is_neq_fn(expr const & e);
-inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
-inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_implies_fn();
 bool is_implies_fn(expr const & e);
 inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); }
 inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); }
+expr mk_neq_fn();
+bool is_neq_fn(expr const & e);
+inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); }
+inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); }
 expr mk_iff_fn();
 bool is_iff_fn(expr const & e);
 inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 08c2e7e36..1b38bf910 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -48,7 +48,7 @@ class type_checker::imp {
             return u;
         if (has_metavar(u) && m_menv && m_uc) {
             justification jst = mk_type_expected_justification(ctx, s);
-            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeUp, jst));
+            m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
             return u;
         }
         u = normalize(e, ctx, true);
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 29cab995a..961f04760 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1136,12 +1136,12 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             if (is_bool(a)) {
-                expr choices[4] = { Bool, Type(), TypeU, TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
+                expr choices[3] = { Bool, Type(), TypeU };
+                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
                 return true;
             } else if (m_env->is_ge(ty_level(a), m_U)) {
-                expr choices[3] = { a, Type(ty_level(a) + 1), TypeUp };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
+                expr choices[2] = { a, Type(ty_level(a) + 1) };
+                push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
                 return true;
             } else {
                 expr choices[4] = { a, Type(ty_level(a) + 1), TypeU };
@@ -1210,10 +1210,6 @@ class elaborator::imp {
                 expr choices[4] = { TypeU, Type(level() + 1), Type(), Bool };
                 push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst));
                 return true;
-            } else if (b == TypeUp) {
-                expr choices[5] = { TypeUp, TypeU, Type(level() + 1), Type(), Bool };
-                push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst));
-                return true;
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());