From 1176093afaf40d2ab168228b1740c13227a09449 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jan 2014 14:42:00 -0800
Subject: [PATCH] refactor(library/simplifier): simplifier should only use
 homogeneous equalities

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean        | 126 ++++++++++++++++-----------------
 src/builtin/obj/kernel.olean   | Bin 24110 -> 24749 bytes
 src/library/simplifier/ceq.cpp |  13 ++--
 3 files changed, 69 insertions(+), 70 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 2c5770bf9..c09f11449 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -77,14 +77,14 @@ theorem trivial : true
 theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
 := H2 H1
 
-theorem eqmp {a b : Bool} (H1 : a == b) (H2 : a) : b
+theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b
 := subst H2 H1
 
 infixl 100 <| : eqmp
 infixl 100 ◂  : eqmp
 
-theorem boolcomplete (a : Bool) : a == true ∨ a == false
-:= case (λ x, x == true ∨ x == false) trivial trivial a
+theorem boolcomplete (a : Bool) : a = true ∨ a = false
+:= case (λ x, x = true ∨ x = false) trivial trivial a
 
 theorem false_elim (a : Bool) (H : false) : a
 := case (λ x, x) trivial H a
@@ -92,14 +92,14 @@ theorem false_elim (a : Bool) (H : false) : a
 theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
 := assume Ha, H2 (H1 Ha)
 
-theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b == c) : a → c
+theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c
 := assume Ha, H2 ◂ (H1 Ha)
 
-theorem eq_imp_trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c
+theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c
 := assume Ha, H2 (H1 ◂ Ha)
 
-theorem not_not_eq (a : Bool) : (¬ ¬ a) == a
-:= case (λ x, (¬ ¬ x) == x) trivial trivial a
+theorem not_not_eq (a : Bool) : (¬ ¬ a) = a
+:= case (λ x, (¬ ¬ x) = x) trivial trivial a
 
 theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
 := (not_not_eq a) ◂ H
@@ -169,10 +169,10 @@ theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠
 theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
 := subst H1 H2
 
-theorem eqt_elim {a : Bool} (H : a == true) : a
+theorem eqt_elim {a : Bool} (H : a = true) : a
 := (symm H) ◂ trivial
 
-theorem eqf_elim {a : Bool} (H : a == false) : ¬ 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
@@ -194,31 +194,31 @@ theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
 := assume H1 : (∀ x : A, ¬ P x),
       absurd H (H1 a)
 
-theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b
+theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := or_elim (boolcomplete a)
-       (λ Hat : a == true,  or_elim (boolcomplete b)
-           (λ Hbt : b == true,  trans Hat (symm Hbt))
-           (λ Hbf : b == false, false_elim (a == b) (subst (Hab (eqt_elim Hat)) Hbf)))
-       (λ Haf : a == false, or_elim (boolcomplete b)
-           (λ Hbt : b == true,  false_elim (a == b) (subst (Hba (eqt_elim Hbt)) Haf))
-           (λ Hbf : b == false, trans Haf (symm Hbf)))
+       (λ Hat : a = true,  or_elim (boolcomplete b)
+           (λ Hbt : b = true,  trans Hat (symm Hbt))
+           (λ Hbf : b = false, false_elim (a = b) (subst (Hab (eqt_elim Hat)) Hbf)))
+       (λ Haf : a = false, or_elim (boolcomplete b)
+           (λ Hbt : b = true,  false_elim (a = b) (subst (Hba (eqt_elim Hbt)) Haf))
+           (λ Hbf : b = false, trans Haf (symm Hbf)))
 
-theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b
+theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b
 := boolext Hab Hba
 
-theorem eqt_intro {a : Bool} (H : a) : a == true
+theorem eqt_intro {a : Bool} (H : a) : a = true
 := boolext (assume H1 : a,    trivial)
            (assume H2 : true, H)
 
-theorem eqf_intro {a : Bool} (H : ¬ a) : a == false
+theorem eqf_intro {a : Bool} (H : ¬ a) : a = false
 := boolext (assume H1 : a,     absurd H1 H)
            (assume H2 : false, false_elim a H2)
 
-theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a)
+theorem or_comm (a b : Bool) : (a ∨ b) = (b ∨ a)
 := boolext (assume H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
            (assume H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
 
-theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
+theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c))
 := boolext (assume H : (a ∨ b) ∨ c,
                       or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c))
                                                           (λ Hb : b, or_intror a (or_introl Hb c)))
@@ -228,118 +228,118 @@ theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
                                 (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c)
                                                           (λ Hc : c, or_intror (a ∨ b) Hc)))
 
-theorem or_id (a : Bool) : (a ∨ a) == a
+theorem or_id (a : Bool) : (a ∨ a) = a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, H2))
            (assume H, or_introl H a)
 
-theorem or_falsel (a : Bool) : (a ∨ false) == a
+theorem or_falsel (a : Bool) : (a ∨ false) = a
 := boolext (assume H, or_elim H (λ H1, H1) (λ H2, false_elim a H2))
            (assume H, or_introl H false)
 
-theorem or_falser (a : Bool) : (false ∨ a) == a
+theorem or_falser (a : Bool) : (false ∨ a) = a
 := (or_comm false a) ⋈ (or_falsel a)
 
-theorem or_truel (a : Bool) : (true ∨ a) == true
+theorem or_truel (a : Bool) : (true ∨ a) = true
 := eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
 
-theorem or_truer (a : Bool) : (a ∨ true) == true
+theorem or_truer (a : Bool) : (a ∨ true) = true
 := (or_comm a true) ⋈ (or_truel a)
 
-theorem or_tauto (a : Bool) : (a ∨ ¬ a) == true
+theorem or_tauto (a : Bool) : (a ∨ ¬ a) = true
 := eqt_intro (em a)
 
-theorem and_comm (a b : Bool) : (a ∧ b) == (b ∧ a)
+theorem and_comm (a b : Bool) : (a ∧ b) = (b ∧ a)
 := boolext (assume H, and_intro (and_elimr H) (and_eliml H))
            (assume H, and_intro (and_elimr H) (and_eliml H))
 
-theorem and_id (a : Bool) : (a ∧ a) == a
+theorem and_id (a : Bool) : (a ∧ a) = a
 := boolext (assume H, and_eliml H)
            (assume H, and_intro H H)
 
-theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
+theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c))
 := boolext (assume H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H)))
            (assume H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H)))
 
-theorem and_truer (a : Bool) : (a ∧ true) == a
+theorem and_truer (a : Bool) : (a ∧ true) = a
 := boolext (assume H : a ∧ true,  and_eliml H)
            (assume H : a,         and_intro H trivial)
 
-theorem and_truel (a : Bool) : (true ∧ a) == a
+theorem and_truel (a : Bool) : (true ∧ a) = a
 := trans (and_comm true a) (and_truer a)
 
-theorem and_falsel (a : Bool) : (a ∧ false) == false
+theorem and_falsel (a : Bool) : (a ∧ false) = false
 := boolext (assume H, and_elimr H)
            (assume H, false_elim (a ∧ false) H)
 
-theorem and_falser (a : Bool) : (false ∧ a) == false
+theorem and_falser (a : Bool) : (false ∧ a) = false
 := (and_comm false a) ⋈ (and_falsel a)
 
-theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
+theorem and_absurd (a : Bool) : (a ∧ ¬ a) = false
 := boolext (assume H, absurd (and_eliml H) (and_elimr H))
            (assume H, false_elim (a ∧ ¬ a) H)
 
-theorem imp_truer (a : Bool) : (a → true) == true
-:= case (λ x, (x → true) == true) trivial trivial a
+theorem imp_truer (a : Bool) : (a → true) = true
+:= case (λ x, (x → true) = true) trivial trivial a
 
-theorem imp_truel (a : Bool) : (true → a) == a
-:= case (λ x, (true → x) == x) trivial trivial a
+theorem imp_truel (a : Bool) : (true → a) = a
+:= case (λ x, (true → x) = x) trivial trivial a
 
-theorem imp_falser (a : Bool) : (a → false) == ¬ a
+theorem imp_falser (a : Bool) : (a → false) = ¬ a
 := refl _
 
-theorem imp_falsel (a : Bool) : (false → a) == true
-:= case (λ x, (false → x) == true) trivial trivial a
+theorem imp_falsel (a : Bool) : (false → a) = true
+:= case (λ x, (false → x) = true) trivial trivial a
 
-theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
-:= case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
-        (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y))   trivial trivial b)
-        (case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial b)
+theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b)
+:= case (λ x, (¬ (x ∧ b)) = (¬ x ∨ ¬ b))
+        (case (λ y, (¬ (true ∧ y)) = (¬ true ∨ ¬ y))   trivial trivial b)
+        (case (λ y, (¬ (false ∧ y)) = (¬ false ∨ ¬ y)) trivial trivial b)
         a
 
 theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
 := (not_and a b) ◂ H
 
-theorem not_or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
-:= case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
-        (case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y))   trivial trivial b)
-        (case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b)
+theorem not_or (a b : Bool) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b)
+:= case (λ x, (¬ (x ∨ b)) = (¬ x ∧ ¬ b))
+        (case (λ y, (¬ (true ∨ y)) = (¬ true ∧ ¬ y))   trivial trivial b)
+        (case (λ y, (¬ (false ∨ y)) = (¬ false ∧ ¬ y)) trivial trivial b)
         a
 
 theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
 := (not_or a b) ◂ H
 
-theorem not_iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
-:= case (λ x, (¬ (x == b)) == ((¬ x) == b))
-        (case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b)
-        (case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b)
+theorem not_iff (a b : Bool) : (¬ (a = b)) = ((¬ a) = b)
+:= case (λ x, (¬ (x = b)) = ((¬ x) = b))
+        (case (λ y, (¬ (true = y)) = ((¬ true) = y)) trivial trivial b)
+        (case (λ y, (¬ (false = y)) = ((¬ false) = y)) trivial trivial b)
         a
 
-theorem not_iff_elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
+theorem not_iff_elim {a b : Bool} (H : ¬ (a = b)) : (¬ a) = b
 := (not_iff a b) ◂ H
 
-theorem not_implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b)
-:= case (λ x, (¬ (x → b)) == (x ∧ ¬ b))
-        (case (λ y, (¬ (true → y)) == (true ∧ ¬ y)) trivial trivial b)
-        (case (λ y, (¬ (false → y)) == (false ∧ ¬ y)) trivial trivial b)
+theorem not_implies (a b : Bool) : (¬ (a → b)) = (a ∧ ¬ b)
+:= case (λ x, (¬ (x → b)) = (x ∧ ¬ b))
+        (case (λ y, (¬ (true → y)) = (true ∧ ¬ y)) trivial trivial b)
+        (case (λ y, (¬ (false → y)) = (false ∧ ¬ y)) trivial trivial b)
         a
 
 theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
 := (not_implies a b) ◂ H
 
-theorem not_congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
+theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b)
 := congr2 not H
 
-theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
+theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x = Q x) : (∃ x : A, P x) = (∃ x : A, Q x)
 := congr2 (Exists A) (funext H)
 
-theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
+theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) = (∃ x : A, ¬ P x)
 := calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not_congr (allext (λ x : A, symm (not_not_eq (P x))))
               ...        = (∃ x : A, ¬ P x)     : refl (∃ x : A, ¬ P x)
 
 theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
 := (not_forall A P) ◂ H
 
-theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x)
+theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) = (∀ x : A, ¬ P x)
 := calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x)
                      ... = (∀ x : A, ¬ P x)     : not_not_eq (∀ x : A, ¬ P x)
 
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 4e34ee73e69d8f13454c5cfd262cc9b22e4b8ea8..8bf6de6fd17102a526c22217279f385cda79a67c 100644
GIT binary patch
literal 24749
zcmb_l3zS_|c|PadbM8!pi8U(G@CYPK2rUXk*GfA9S{M>Sl_b!hfM}e|oPp8FOfs3_
zjXXpMz7Yipf>cq&iYVGvP;6DIC?K>IT!Qrh)`o`)f|Ufs{@?fQefGX*?o1L_vlcu5
z-uvJGd;j}&ZWtXd`$h(bhRekLNhd~zPAkVYmPvMelBU*bMYeWyJUOjzEXj@-9UV?O
z&}<!RCx(W{hendd_}E05RJFmrVH-YB4kp>^GuM~L8@{8%VI3$N>>e?)&8#oUM3>z~
zfxlFskG!%>M3WVx<9*{pqa(mcvu}P5e<uqwl(|@rj*%o<NTkVf7uJhxE&fgl5S|Zc
z7fJ@GtCjRQ=Ohhl-HW7ORO5T{f$GG#S*_z9-t?KMk6QMP3;;3NwJ@&uQ&e(D21tWH
zT_|R9%+R{^!$ajpG_)JnGNLB=f&~;{J|%xiP4WXzRwwArsY`xC)JG}GGln*fZ!~)z
zo{(C@z*Uub=}0+><(?qAJHfpG?%}mN1GS_}RhHDWLp(N+J}`FoYIQW7qll-7m`4m!
zCy5S%`=Yh0lO>9dqt~s+-^o7qUz)aRcqoHu5mnho(K1qQAo_lV>4-nOdna{xCpo#%
zxzJNzV3j)chcCS@qQ4*+KQ+n9b(OUWiaHBqI%Elg)Zzeu78T1!6bOsh)ptgc_4nCS
zg3<A(+02$7thnvSGEO?{TfRt5v{k1!VKG0o5e*FM0HLvRaJY@3X*oKwvfOKJNSb2I
z#)-8XF+rVWJn7&a9}QqdtJ=h>Bn0bTibp0rtW)z|fIZ%pi>;EU_6IBnCq~LMT6i8|
z0>~;9(_&=MT3kqh(A;KrO40;$B#Pd^!USDj;r37p8gec{O3~$|_-h+lNzpevJV^@B
zUeU~YD{*LV6DP1B#pBEcl8zcLX{oL9?3Np~hUttTp_vu6$4nE3g^PkCElv)GG|5tf
z7%Is!rNG4uzyj{bfzVSpQ3g<3f<iOTi*c;Acrivs$JY#vjE{|08p4|xlgvOdlc9PN
zK+VWE0c2MdJ11I;lq$#jj7}9fM*tW08ziu@(@RF1%|)Xo^qT=HiM$2i3UXZoaOHlC
zF?h<{%=QxqqM&2P0NKQq{d@N%KH}N+&-HqrY%Q4t9UmJyZK!XUNQ*f~&jd{Ji{YNW
zwHqhK23m|F^CP@u{+Srj$sx3~>{FsuT2bqnj7&yx6?XlG;taOIGM5i^v;10&#!6+*
z?gpqN0Z2ZqxYLBP$EoNR_n`p34d5n<_jZ823sHi#)YQ~uKMhJqNdY*Ou%}qXtk#-T
z4>^ZZe}J|=rMBEWeC37e1)a-b&9%0H=pVJ!tsF;U)690cv8E;^Slq5rrXB^+VgVVy
zI`Lko@K>-=Cfp3P4)Eq4Vof<b6lG-};+??i;$TLRjK~GJ6WKobD2n%?5J5m)pgOc}
z{hINyz7edGPMyemw6b#}hFn^?%^;zdXzwBG34mgKS^!TEAS3%y;xbGxwG`l}%m)@j
zqslVl*5ao(#4I=Lw4~jj8bXh;Mkb%25a*&>0>2}G=LPV5fD-rufHwz$Y1YfpSfXGQ
zw#t8wHGBC@_MNlz%^><oN_i1LN%^h-UL3$n075j)=Sfx#qH=yyUYerHeD5>@UQ}dK
z{AYU$@8hBy9Arm2iW^dLQ-*jC`U^!`ODKOA9Spe;$Q6UOp?oJsD3sq1P>O#5;GI$=
zNWje1rM=?2fl*r^5b(-R>$Ft|N-aB~X?7LX%5qdsF?|__&<`I9ApJg@tsh3~%qlK=
zx;c6K(W;<eZm+V?2d&xV?*36*ulm-HYM=a|-@1kUwGkzm*#?X#9n4h102N2R7Z3xl
z^5zxR;&>?iPs$o1ru5A5G(a#ci7F|74E=J#H37VqqiBGS1Kgt3Y6IY;m*Mgdz%VT;
z>8`eBIR$~hiEV*^?cL=3V_V9#?x+K5vr$N_zXvF>J`uoA0(?fY!1;zfBRjS4v~o>(
z#`>`&4H|BNO~r7F#5EJBPMPKXPlH5{Y!12O$<72%!?#-hI>U0-j}?p#c2R<rgP#Fq
z?NB}gP<q`Mz|R7F#zdCmx`KhXSz{!&<T=_MBW|!!PL#27<LK~d<-zUEd~m|O!z{3o
zHh><be?JdU5-}+W{DL*62z%w6EkLR^C^uQf2jIxS<b7HD@B@i1$}tBZ-5_Uw33c)P
zasdAkpfbfj3FK}zvc?0!P9YGNdh6U`gCZ%hvQ80&vJRyR){$tpfwM&WY5>1xU^-8!
z;5sxXoKehI)kL_}nrr;036gXk$VlC<0~FJL3E;mPn9idCpG9kz_#+6~^1t1h9skiW
zIjKc|#b$M0ijII(Mw$PcATCk91yHSbsMT-vw=i)(hsNLs5%JFWhV>~ccv)bJDp2H9
zBrFhdVG_bszW5HhB+H!v<Py|nk*a;K)(p?~+lE)Mt?#WW?){+Vwn1T{P=PLHPM^D|
z9gdB!;fQT0l}YXfDB11_;P(S~uYu`O&ba#kE+hCKK-d<1YG)!@APVhr29T~#QI_*j
zc10}%%3e3|aMeWb0E!-mLVT=u=?XgOVS>OYeP&5lpt=MFb6&mhw!F&_{3gN<>=W@8
z8IJQtV#eqMIYsjW0A-pV8kD|O$3c)Y6cqBA*7?6cgN^k5)P$_6Gij?|0f+vna?<_Q
zB2RBTa~-zOhXbeGt&I<|g_03iimxAY0R8e`02S*$0Vqv=3UJ{<l>I0a4uI6p^NEh~
zG-3~h<yJVLR{7x}8|Urmx9HOdO^&>?P@u17WP<r>DpCTJB0mSHV=DaZ6nO-o1pNg-
z;r=(k)l~YI1cQ1CBs2<@>J5+?yQri5<74D!hRlnK6)jhx55H$qbPoF&Z=XiWH9O*|
zZt$nZ^tafBM%tB)lJQZXOZCS9%7>2wl<H3yl)jtsL@M0%MpWh#Rg(%HvWbF%%!yX{
zZ;Lg1|JnZE^w~)-*7!?5dNt@5m}^r&OVIl2DInZ$P)O+~0ZQqo07~iK0+fNCHYmM{
z!>}z$H@EY5$$t5}8)Ly%c|w7Wwhkne^fG`!AX(Cf!>_H6;eey487Mm9?O>!=+~dg>
zY((#s5TS~W^lA$Kzi5<Aeh*MK(ZWfDt!R}^wi%Ruj;&b4(wo}ZM5t|TGSzJOoe`_l
zFE`kktL>49M+`aY4>rQ($`=5Bm`VF`fQwOd1)Eb`Mm~G!m(AYr&l|3?VYy*&3br2s
zLGDUZKw_H`{)o2NC$b&6xKB`!hUR7}XiWfrG(<7B<IgE$*pF78K7vHTH5;x*@#k2-
za`gDryt;EfIuuL<<zDEV=IEklQ`&%+aA^~*D~Ui;97~WAa)nO0Ag<QhbF7JV1_mSp
zq#hhdmc2!GDmv2#Bu9w~C0M#Iz%x0Bt<XN@Qs(nQ+OVd|>$Jk6wpMU9^}8V3Rt$o8
za&pZIG;j}D5@aBz1Z4#-pR&S>L4cu@{uw~wz69XOGzj-ps}bMn570`@z0%GkQkwcw
z$5nNufuBBt;g!<6TBTL#wmM70mF+yQ-B@YLBiSU$GR|^9E*dIP(;rfmm!nS>*bSg8
zFdLxa;1vKB2d@OEIG6*F2`=3oAU9&^9sp^Vq#veMvg@VQ$r$Dk;{-V%%V;H`(MlZ*
zt#nsz#FTA_NW6@J7;-15$@Xqo0}aH=UR3pwE>ZpcLi#f6Y~nq_&2GMd`3YXlv{fLH
z?9t3L<#Z9CIZZ`fwxoq8O}-@<>q5eybT8Cp=eYp)p!N3#$X#8!k3rch*g6m39C5;q
z3=x<eN1!@}EABP%cCoJXehy`B8DRM^TQLfoRQ#RZ&lsdsjC`6>)4}DubWg*p)??Yl
zzZgt5jD*1M9^{j`AfGXIBF*<lmo)!#fYO{hRLwCiKXbX6@Cii|6?!F0x=}tfAEl@Q
zqR{@3nqnrpLmDoh^{^x1%xjtxaG%|i;16!H*5d8L$&a=kvY{w2WbC?wP?wW9sRVL^
zKAT3zIVL+4LZtoe$kZ>msYWNLF4J~>1hCC4lW-hR#_RjEpCF1OiCv-(gR^CZx;93=
z6kQaY^Nfob(d%m+8@1Mf22)9PB;(>&-5?T7KuRUliXIX;p3=NeE>W0bsdRHukp*2G
zaZreLv1)b{idYLtfY#U5I8uy=V=qv%*ISWL7zJ^p4Efaz!tq3JYY=u<Y4|`eP-++&
z9CSA`Xgi|q^`nm}h`@--4&}}_1sxwrfMgjz(~uz?7wl^MEUUtHIff)1HK&lq;=+2;
z!_lu`JOUuMk{N<VoEDovS_L?0vsD?iZWH9?_#49yyPPS+Skz7ozR{%1z))hqtH~l{
zpGXXQ2lQf)$U{KtMNxT9Vs%zA;JUqpOAS{N+O>zhEVaDtxY^w*U#b)CtcVL}ybg7V
z%J|`BJVi~h{AXvIs6a_)E<{OFQc@T&JrrH`^yswd)y>hj(HdnYAV?o~we$@l1cm+W
zM0R#yLI(jQg{~13o>#K-&`1hQ9f1Wek+TcYtsWxcoM4vf+qiMGzshoPBJ2lR5<ghb
z^e~qbpsJIt-C?3@HAfLVK7el^SUElWU=t10Xo~@MT_dArAC$g<G)1ObU11C^I<hN4
zqB3=MWw2C<o*tpk2h2sH3`B*19*oy)D!Z*JGYzl@Rm=wk4|6|_oNY$;KtLxo#wpw;
zy9J*}PT*vhcr7mrvO>RfX-!s*q1Hh_NdP}mg6vv@u;?q)(xt65?fwG&;j0yitq7=T
zbz!g!RhKCkP}Hrm2bUiysHh?iXl6Ho8=qHk?HIk2!%l9&2yAFA6@_)Dv~iee*;g?L
zs^jnMt3fq}OejDi9c1B<l?>%a;*kqqXiYFa{YH1QQw!G#&fHv*zTV`R2C_TU<%GMV
zCL9M=oH;l<eOlo<-CU$_(ZzLJ;UrfO?ri`I%1|w5**(_g#N^VO{w=T)jpcSCE!pB7
zhL4E0XBKS;FicC!Fu+3e|0bCqzgA|LpjvDAV4gjQ`sS*L*=|o^`j5QDb`(_V3jfsF
z#FXD|WcL9{Bc<-!(NM+bc;Cc$^nFWYXkhWmS<E(|ULbC>9|3#~(n+fM0I%6MeLJ|=
z%wzD+0TD%H0ZJQD*J8t+T9^WSrO2Lefs@YTZXvk^_{y7ZX}O&(Oce?`tvI*VoBdpR
zVuAH!Poi6cpnUce>KxBTZYZ*+YmHvv>1KCOkXmX2@w6LM%Xr~Z&F&W{L0~2|su>gH
zWrunp8G{H8*y%NFPVhx!xYovW9vyTJILSfh2JjsODOtaP4NR=Y3@37fABxDtJ?Mz6
ziMn2OY2B2^X{i+StoucSKxt;>tazm7JEJ1udaJtIdIUpDE(j9|*N$&PZmjsapn)*E
z`FKF`m}VBwAsZC#NMTUQ?MMiT#@^`nA<@`7NJ`_lfy%gU56cjadO=`wEYdXjj3R}6
zrYOA_6l#g3frF_NPMK~DSWXkAmJ8TYMdS9Cm|za3W9^SOfktEwZVs_2Mtg%B>u8R0
zpf^_Hw!|TPX%yjjdu(rMp->tEjuPs<0P6-h#M&AX4;&i@07)Zdj!V!GP0re9bMS1u
z9SG)dI$L-8ejr8WI1=^B97mD{j|kdkh1|glI)!vdX=?NdrM<a?19J`WJFclB+TRCo
zT12bThboDakH#xu<5+ZTt_p^UXVE@FJquD-ZYXSgdIgBkC^Z&utf-Su#bO$#W5f&;
zi%6Q|xXdMIq7{wFB5#dpA{uztpwM#pF@Wtvd@DL?R=_tM_$J=#8x9}zF9WNXkAc{}
zr&>T~p-yK>@{gmg{Cpij<h;l}?MP)$aITOPgKnlDMCDt~JQe@O{u)#@C<kzSq}Yy7
zI;2jC)2B`edT`t7?BuT=by^9=au;ijGAOkLV|5(+6hPVM(*eA}z(z?~FRv70s&AaD
zG{?h5NcQ3S`Fb1bZX_UB{4<N{7OkDp-D!IcgoyliBkGdxvjn{Xxo2qaitKEvN>V%Q
zzwCi(P=i~@y1hN)X<{I|C(xLHv~?P2t9)k1jruDTk2(DO0ho<V6}cpG+0E#aNxl%k
zFLFT5Wju&Cu9eF^1LSrt`@A(rF0<>Z9h`H?rpS{Zt}Iy?lzs_yN%>`h-hNX#u11Op
zl<7OVO{6_}`GzSxl_zSHw2rqn%Ejcd6O*%*hFjHI8yoa{oiGeg`5o7R+j0DjtwiO0
zU3A|{V-{AXw*?UA;l_<M?<a_q#y92tTY%io`(Lr<*!%7mMbl<oka{KrCl?{*TOK#$
z_OAo0p6nyVlvq3;nvB=72`4V=JCu0e5CoyC>yyq0-c;cNF|P?Uwx4WmdB%^fw&TRu
zK)v9hgnI`-8R*{v_-%mC)cuD8d*c!L?`yzl=f7`RbL2lhbGDhk{(YrBWuwG$Cpbv7
z?*{OD05>hPBBM`;z?U~|0}zUlT)axFZo$8UVg6#+J`Kh1#Hw5B!!a_+{m+){k&K(6
zq#LsOR~+6WMJZqv#>|bv2%dBAMSf$|1DqvOb*zHK>D|D|3El%xFG}AB*v-~^4Qf0q
zy_;yBi-M$s3Gxh$z;A3t@f?EMNwc4U$>}KcVcH1<QAGHtR@S=9D*oLJi|63znEk}a
zOi{N~H-^<VK*`FWuze_?G|QQ}H}&}e#z<kl2krsYQiK@g$#?bh(T!9U-Fw@A`Aps$
zq;ROc>Z0YPx^h^~7JW2970Gihcq&Rz&u3K<A;|Tu3Q+P{RwQ%D?B5AOi?GYgXJVHb
zjNvC;-6Af$^Id}x?CMjh^afSr`v<{7rr;?-zW*^AcdgGsgk-+2=HP!~Tomh-<9=k#
z(Hx9^4~YRG!YBDHNJ}ft2Kqj97jCSaj6VZdch^Bdsd?z%r)D?x)1>=&6T1257N4n1
zcu+O<jBKuJj)%cQ7JCGsEcOdD9u!+F=+g@{*gx-)@qU7acE<a;HTxW)1Tir(I66Gg
z^2G|LJ>Jp#NX9=G=Z8^k1W|f-U~c#9a=pI$n?t)FjFBY@<}nJmgtq=4H11At3qWc2
zC_pW`j~SF7#^06kaa(zSQ$FX_sU5aC(|G|-M#&P+uYR)TR2?8a6yaq$*B2d>|2IMY
z0m||?a0jSh&>;HutF-R)e#8N99P?Fngw^j<^HpG*U5Gw?+)zRqKEb;0DNrrJhLbd1
zK{6{)r*$}qJ1U9N70#mRikdvp_Y?y*I6u*Z7%BBrG#Ub}x;pHkQ0D<_4T=+(KvGIZ
zsq(h~w-*7GJqhIKYd5;9L{9@964F2J{SxhNnTbQF<#V5QAw*@Af&eOWhs43|VEgEO
zjP?P=#x@u+{jC))gm~Ma5PAl!3ZdT_lusxo4CMNgA8k-$n-#p;qPfz$p?=<v#^4|K
zxiR#Qq8C>@i_nxGy&p=XWgFyTUkAQOdU}F}!zz}a6*LCj{A`S_0vX?XFr@SIDuLvr
zlYpm-m8ZG^LvBSCt)efZ$xKn?z4VmfwewQ7z}c^4>rNsAt#mdzKMci00fv9D!dd(U
zfU@`>0rG^vw-`UbHWc<JKTHvaaEYd{qSN1(<r6}Jw3Cs%F3($^0&ch*9QSwpN~xyC
zai)_pm3`IkQWnVBr)BQ#S^3HGn6{<SHb*&&@g8QO5~rfxD7sf!x4wBI_SN25;F6TV
zY|0;sg%W*r!fIrs6BJLs1{g^RSbEw66>XOb=xOcTBd3#~>H#Eg-ll36?_QWdS#Cvs
zEkP)lf0E#f0RDpyX3OYKj>73Uz`2C|i^B3Iu?ftmh&Y1O&D+C|3<LaI5%%1uh(3;3
z`At+F(<ingD2Lpd-)6P^D^SAaR$eK}TAC*j0m!RHIhXQ7)rjl$for6c3&jjuP&cjc
z+7ZX2A}_uR>NjND@R49Otr|1Pbq>0s-vve9dO1fyrHoG!1wn3Civ1}73L}hmcQ^=e
z$}TJTXw^6XxGB?3Y(?x+>`vrQkUzVO@-vUaK<R5K9`%u=yHf(T?m=*WD|7CHgP10L
zC4LYYcN*D!6#4Hkv@Y_H-3Rl~6+LlOH(fT}ImTQt;DP09`tU`?@-^<4hWZ?@a)!1j
z_-V_UwYdCTzD6YAjr`GWP!X<AEF{c=OHno#C{lax0PYjOc>$bnVE!2G0?PU0oFrse
zT0Og}6Rl5Jk!%AlHyT)COgJ<q+*hRW04Em1H?>cU6@#Eg&GO%2FbBB7n8J4FWkm+B
z=+n#UAE<z0Y|5XgCa?}HTRm;+zS!{cZFLlD<UMTuT)oE)*7gO1lf^&@U#V$Q^4{77
zbf;uQXmr|t`5#z+H9;%f)M1)}Mf0uuTFG}|(bDf{b@s{l2pFA%o&$x&u(5)W=`Bb@
zEo>JCtP@ZalIB$gI!P%FLc?(b_vj$?+yZo6hDK0vgHUU<Q@otSsv@0Z=`DEDis)~%
z#spi?H6!$HcGVOnr}4Neo$ON3fHMlr-6Hy31EgW2*@$!TYHM)e7g-5@Nw|A%vC=_k
zMqda>WLvj@RURwmwAx5p=T4npmV$;_uvKug*J&9|07J^3MKML7qiZV)7)%xj3Md>~
z6adx>KGeBB()=_6E({9%Xn9JT0|B<2&eYTS$<2>C3MfMU0^85xKy(KsoY~?40@h1W
zAczVqAw@T19f_HtSnP?${rsY~m({AT*sBy9J&5gKie+x#J$(LXlu|=d${z)%UqRUH
zFRgHy^REKf6Tl?_JOrpqISiZ9Vi`@uI0zq9E6SgNrplZH@RgWr|H1*}@PHxZ&jwU{
zE4D`B_p~!V62{bCot*H1j$NzrTy*i{^QenG;<Y+dxuUcl{+lrcWAE-(94%Xu)8!GM
zhlnMS{Ew|!so?on-_C$O4>w#3iWxQf%+ZtqD{}GT+EnFerj9poKFD$pw6h!ncZ!Jz
z%1G!`QAhX?*O3{pA7U7%cas}kS{y@eb(aEl<^R7kIrZv`mVDS5)PTA9aH}5djtW|7
z2B4F-W2yqjv9>{`1ih+_d87P&3V7@ZoM1$zVG2{sL-+hvKSm0KD+?}I>Zzy3;y4i5
z8^!TfBujh(fs&IGNOdf0vnQ@^(Yiqo`HJjy_J{rQUl&$p%h^Nl=m7FINSm+Mh1S;_
zSey%E+m_D$*ggw$C_|R>7c_vF2=K`!D%n*idr|m{#_TAoR9e|)dFMBtAn=&WgoInw
z<ae6cl~jvoap`ibp}NcngFBG>VIi!xMz@iKAM(fG_2QjPD|KN(y*p7YLnHNNBb07g
zQr%;N;WvJ3MVNc~SeLR@X5oFb|0Rw$%T6s8#-dmnEfD$_E9e5Q5XF0G5^cQ*o@hgy
z9Zm}1n*w+;`n5v58Q`_@IrCU?Iq*s}e;AO|r;Yg7S9}Dmm40uu$|Se%Of1{@;#?H(
zqwGpo1lL-tQ-g_1?xZ9FDP$bGk4X<+HfgB`ii=$ky9m`v_P1K4l3m|J+RqVp>aYX~
zk4G{4c(=8<sktw}IVdPIL`iomtke$&rNa>V1->nSZx7(Gf%)ScwvHgeHx5C>Y_^{j
zWK$gDH)M!lxo{UnyhqXO)ko&owP_;b8>KZPcJRYG&q&U$BB=Wl>>H&Ax0rND!qq>P
zr9$HL*#%Yq<9q&&bF#H}YAV3cv?V8QwQVvk#WECMqnXCQRwmsT!0`Z11n@MV{(!^I
z0LZ;ktdX}S*m7#<2Z1u_r$A^RB#jbvCJpMpMJAQRTkFOo3XSP@T{gD(o?j$3SZ%Vk
z{-lX@JJrJ+b5?mr0CDB*TF(#Q1!#;XmRl6CYDUrAx+u8Y0bo=!>>R69TIkKtzPnj7
zV2`b1Lu>6{hrnbz97FJrFsvtF>)*W>6YB29Us~t<t)HTC7CL%S@JD$G>vm%aANmez
z{VvpXmq(fki%Zbjy}$}yf)vlvg;+uLoyeQrI#=+KRd)#Fwk05L@!U!bTLSNDBaMV9
zO?Y#fU5I`;+kmER;Fgc5pVuq=VFt<Kg+>bS`=<053>0-hTvzZrYgCGD9#=c?el&tf
zQ~!`8b-}(}zdH{9R7Ov?HA*IuMgmChGOCLVu(9k$RA?Y^F7iQn5!(4LKDP5^cn;oq
zU-D)s__n|?RL>I`S0TBOOOIT51rWNC*ur_C`3kER+pK85vR%)!?1tO(-K@|LpLH6C
zcbl^dw4Q(h_2T#5#uQ9n=1Wk%IA<`2i#FO@k5c!c5%prLw;Pt!7Q11w36mh611|LK
zIq}|2Ae2l!3Fe@iQK3n|I<`Z_Rw$xh&B$<91C`GZ*~b8e*l!-d*y~{VGV~pbP}Wuk
zn}h1()#d@PoIVc61|qRpqHtAAJ&iUVLnTvd?^Ba{8OP06RcL{_h_L>2Jj?R4j0gpF
z?;=D2<tB#2J>K%zsJ6VmwOW3M)6c#}r~MP0b;Oy7PT)<oLr4D@{qZS)^2etEDv)mg
z82RHUt2U2z)4X}qepc1%S(P2!%Q43FpwL4t86#{P&!f>6mecV!pM426`H%a^e|&V2
zfOhVe7qLv`XLVbtpHGwqxqr0)cGkNekeY}w|I7w3!t`=SuYQoR@mw$<>dlqp!=RW>
z=44gGx&SZEPWSSRx}*lAr?n>mN+7aeRHEKI4n1HNmZ$5jGEH>sa6${pS@M@PmCNXq
zD7T^BWZ?7ZHM<4kC?viFP$BVUfc4yleP9#Ex#qfBZex$aM(=~Tdy}e7Y$TiZL*z&(
zefJ*cF_>Xe9upe!SaZ3bO<%NHi@jRb@*PfNQ<{s*c$Cpl=R0Y0Ih>z;#R_MxTLCJg
z-3Bn4LFZewd4Z3_^QW9a<fdE$iMWa2llPP}=we#F-*D3hQQW0*L7$e%l-_SR3Oj7`
zPCwYHHjrU?VKqjVPbXDz?&`o*utu29k3_M55y5CKBF(!<^E`u_A3*WmR%*@n154Dr
zSuUtlaVl4Aw2im~Lm)P#Zfpxy#AM3(9kUWhN!Q#Ce7)t;YiFTO<5rm{yxX4@$%oOL
z)$Yohqj7?z`COX89x8t)Fgwumpvgte8_!2_`6!2gWZk?5&}9C}l8C=yG(QeJeK!Cj
w(z%YE5B+~ed%AMH{Zs$$8!A=o`>#ZheNQgHmKX;Oxi41Jr6U8&@V_YdKg2R|E&u=k

literal 24110
zcmb_k37B40dA|4l_x>{!CJLfxSduVI2&korw!uk#APj_nDG3lQ2sq4S?!f3UlT0R%
zKrk*qVil}_EaHMIYU>7WsI_$|3X1d*tXek&GKv<&0D|Ds?|t8M?m7RRe**Doo+l^Y
zIp;gy`S!EjKjWk2z}WD}XqmV_>4ve9bIXbKWs<!-NmFaJA{!i^OwJvcNV22G$48S6
zG+W2uhLO?9k+GyPIkBNks@m|ts0|+~hm&mernTkE4d2n>unv?Bc8?j^W;T#yqRZ~0
zz&|R`$GNghM3WQ7CkG}+#>aq@W?%hR{F^MuQ0AI)e1as=LLyC;yR%+ogZMWoK)4&w
z?&J(mS1akwo0EpM9zfE6Rh#$p!_<j!d$o?cXWNIPK1w+-HUz|EkHTifpQ7SJJb)Yg
z=|VA!V@A$dJ33OXM?<@DEhB22&!0~Qy2<&THO>z^U7esiyUzIyQ6IS|H;$~ITyOeZ
znvhz<z*UucX-FB0<^CYLFTn!<?&qc3h+5L6DoaY*p*hx(J}~z6Vs$i~p@=7sIFJ~m
zP7)mi4?=5KCrcC^$DOkl|0eV7Z<@AB_)<F4B8oCk-ZECMBl^LG$%sGudLwmsBRRg&
zxxiDOZ<RXrd){<?M1OuVd3KVO=TzD%$m(7o(;-a|q!cdzXkM{=OpdUKT>~4FY|Vg$
z5|oZV&1SZIq5QTZ%NTUlw|tSBsH;w|!lFC15e*FM0HKL;c(je8sW}?5(%g$}NSb2I
z`VE8Y5ui>po^-H|_XbQwty*AJ9AfG|vd2k!S*PTE0DHYI7h5Gy?GL6L-Y`~fY?<>Y
zV?bIVo8}|K*5X_WgyuA}vyvvDqfzvQDU8wO6>cxNpd#lGBo|$tiz94k#l^tr=rk@s
z`-EoJSFuBV8#`eNQas5_Anqvfl9t*kKizVp)-ajjBviA!_8)fQhK2Kjqs>nif}7+R
zgXk*BGNr)9bie}U$bryXI97&GTY^H7=h-;XT09$L<CFa(W0Mo(m4vV+#w5F;m_=88
zB|t^wX#m+(`Oc}<BB9F30i#oS&QZXH{)P#x?DU*bXLHb~fIb7DlE|w7p1@iA0j@ll
zJ_bvfnc02{K@>FX1Rx7s>A&wF;=`X^{~Ry(>DH2o(aDLCb4Lb7iL{t8x(P7JFNS#r
z2G?(x7-~_9)DQQP`e$K8Cx=ke(ocz2Nkyq=(KG4AmD{Z`6sNFtmbtvEo8|{G8Y`7E
z_JV3Qs!Z~qO&m@<62MmjT)@`X0PI_U5>rVmg(CZ@Ktf6az^Rx!%POX&)+GA(n;Ggu
z)a_Zd<>j8M-=JR5xg6RXv<<_Waa+yGNhC5wvde{?z~a1%11L3)qpO(DN&Y(V7A2!^
zXQR|}Eh%6g?hpFQ(UB<QdiN#qE)J%L$UIzJJCVtgt5LiKg$M%b0@aao*7i?M42)q7
zbgV~~p++MUZL3UVkkCtz>gCiM0BY)U19)Bl>9yO4OBdW`;q9n&1B;<sWspg0@u3Sg
z%XNPdr>jBvy`1zyfMW2q0o)S6*8voRuLrm~Fi16Cjz&ogsFmN%*5dg!UUyBi<nn#w
z@*<EHmlp@{k^pW62-Xyv)3g{^Wvr54hE$cs-e?3otH_G@Yx@Lm)1s5+;FgkeD8}DR
z7UWMY4*Lys(6NHMR%F{c>@64}hrJA-#C<EkTf~0gfVrnjyS;w`MlHo(YAwnz=V-GH
zls5TgpUQcarzoC0_iY?P?bF0!=L)p$!`3SS&Z@kjw}&CR2CWH`4YPBVSN_?WUG`lw
zZY$2f+Hvi4f8aM?VTWu)NoF4d#uW6klomk6k?#Z4y0TqmEp84a@M*b0#6p7Yq5^_q
zNmOa}ouDtN-xa`j1C*8C18_>~%{stIUk}P3qM!y^xx3DqWfV99!`B=E8?@<J#x{k6
z?yv%C`=Ah8?*%Bf-WS041Kc5AV0^>gEjxSQ+_JyixOO5*gM?GisV1BfyQTuw$+N8g
zA&}^m&cSya;!NHYtyRA34a;di7BD)RMQKz9-T}(mV|*B(<oZYeKMHV%u`I)N1qDBD
zjS<`8=Qwu|xWPs_Rwl~z<D=)63)`!CVZzmaFH9q80R4gv{&9ff=o10_q=BiO>RhIo
zLQl2D_?T6^1C9+%-&wVHKal7mAF~0{3^MjjsEdV92k<ih<%6FU$o*)fjk|)Lf+HT|
zwR58linzr3IfEBUJLD>8N34ATGmEt^2JlM;rgN1Fu19mih+@8~Qti#wT$_I<PLj?w
zbSLhY0cz5J58!_on9ijFe}~pC%?~GNJO95~vzvc>LPlzlU%pwLc%nlbg;D1JDu|1f
zuK`r+*VXFxZ&OU%zei)RgNS%ze8u{d6+AD{Mdc_mDiRimI5!FIDqC=|5ij2amcUy%
zz&uquSFIU-+FPu%nzp`!s%BpU5^l2-0)+x7bNbvx>2UCS5l1|ZQkmr20L9Sl0sKw?
z?=Ucx9RCIIXa?VRf$(^+shw)1fylK>o<ly60=4W$*%h@6DSLg4$D<~Chfwr76yjsO
zOIOfHcN4TCDSc*1SD?BC1#@1#@Vfk#A^5F>9l1Ben_d{sD`^oZb)r!4{x?9W=KBVv
zuhM}I<O~IcY^HVo`Dn0_-ku7`syd6h`ZaK9pDHJP&st>Z^_$MYMtLc4+TFW&CtDyM
zfhD{Am;-2+p8%Av{}iAk`5C|k3s9~>A$I_zex5jV7^f0@$?T?9)G9yx$lAR={YHEz
zOmjxwI>^yin;cYivYLXFm_~y99H0)G_W+b2_W~57_W=~{c7UrX^c2A$o*W5{LZx^^
zoQz$RQTFjZa<?J#s^Nr|%glS;ye&Fe-Oc->v9kZ^SgHr}Q)1d%(}l(;-%y78fiBU1
z1yG{XUnKhfT4Rch^TLEwUI46!N;m3V3MyF0Z3#Fz(JK4>()zspY}aq{?4lKG^GiNj
zHON<j1NDSPYF|AC`hSB$LO%phLjM+^gx&#AMts<y^lA=!1mHF8>|L^7_U^%07(jVK
zj*YesB$Sjp_rQ=e>D}Q$!=O9hz-bDK4suV^)2rFzU<*2;^-6Ff9f6~3$vl@x>Eto=
zODD|O(g~L<>EsCv`zVJ!3GiRq=_HPUiYw`4rf7K7h*jd3>+Gb}_DFPvp*chS5ukGA
zp8#ILq<uNS#VERh&dDyrfjzX#wO;XmFkEHBa^3I@)4G!lFhN?=ri8E57W-7TBNq<{
z3fxfLOa-k8;LnDriS77v)&%yWm8Fj&k#JFl%T4?_(XSl6J~gk_F;vdf4IG&lGN(D}
zv}{Tp@ER>`qID$^sEQK_l0&Z0DHp`mT6<13wl-owGDPaZfSj_g$j(M*dYAYpQ6UG%
z90YI^2eB2>r?;Zf=Y_OkmCEYW!lJfXa60w7Alp_9gHCdKO$$_TFQ+6(M@$Jy3tT>>
zg=c^O{X2aoK;iBQ@N_C<FMzAz-|2S&QgSb}Q;CG8yp(ZOU1;E^KgaM&=sm2`Ds)?!
zCE?0;me+2qG~t=;lVyx@OyazuVm199MR_**q=DxElm_+zC_i{EK>5M*0Ll+$17w0r
z_XW6&#P$P7y(DX(Y6W&5wa$s54o#e#Vqlg~OG2ZTI_O&I9*ibs8zMGABcpqU+zD#Z
zy&Kj*1F<stEaxO$qWb%VbZ<jz;zhwlH(#-QfLD>W3e=MQnwdgQ7XgZC3hKg%8lDz>
zOEA{CghA;6s7udt0PaVH%>~FzmCiFLdk$L<1o&LdgdG_?FguCBR1g07p`T8Hx4Si^
zcXH@_bPut-o2{s0lZt=SJL!Yuik?qZDjZzSOZPXtYCV=-{GI=F#SDOIg55oVIUt|W
zqaw)<L7yZ)6rd#M4plM6<!25z6F#9RP$5^cL=waP@#=-DKcuFJM0ZHTb+Vpj#GF}8
zF#+@0JqiBcCTkF{4~~Ddkzsl9-=Hp|Fo*;$LMv~xQk+||C73iF=tMII>x!Bn8<%M-
zJ_ZDf8k>C*P<EsS5=60-*rkD_lbNlT55}ll(FN<u*SSy;y}pjIQR^6JFim7jY4cxm
z62$}Nk1qQ;irsIKlI3_<{M?N46-eMnf<g-AWk;e|isEP#G4Glet;=gOl8tD_KA>jD
zS&@(#xn(2*=c}oK<7ZX_yQ{={7$#7#j|>mHyB4$^(e^^o`w3W}k7P@@mrX&(nOhkJ
z)oK>Ryqg946dyP8GWZ{`lMb>*oh~k{o<e=j-<WB*CCtu5tHbiyoYiZMD>|dw%=pMX
z((uD>WroQYg~|Djk}ktE^6+B;E<)~zCbxGux0FQpX_URPl9=hN?5(_5Y2_FrD8B5{
z!d`k>-d|j7f~#~7QrOEt9if#SUWU3DTtTp6&{hd!b)zwe_H>U0D5>nqHYwAvJ@`2p
z`gGfK3kF2l1PGGCT?c)I2tiDLqmXS3lh7DINrhKULPcepL4rL@31JFe{AOFwtsWv`
zZ*Te;SigRJO_iDA<h2H9Ng*{uNp9MpH1e_sU1~LP3BEjluOL|IFT1pf2FfvIfL*Le
zmD#0|GLR;t6s9YTxy#06SAs;P;OxqvpAtR2LhlC5bY2FcLO>73({M@IV^t|<h&`xY
zZQXK|UUoyZ+12PC3h1OppM<fbtzZf937qUAFXd%{SIC$4)p*qyN*x#!2e2MF$gVR8
z%d;FT<x8rZP&%vAB-^rkO{y(HGZbB_pc_%PN*`QIB%pkWIG~yF3cSPl(n$0s9o#0q
zo+@liO3fDYG5kyvpSOY*!N1w(gOcbdp@6PaFqIBDjV2vE7(&-3o>GKkhYzsP-D#br
zP8+KOW;zToVu|4h8=yV=N{uBBtmY$2+2l@H>Wo>6u9G8{#0}=-E;M~Lz=AVxC1^!<
z8wxSUMKe7fU5UnW`A=!O#G3@4<g{0TmTipIqA&`u5Y;1-?)behyAyp}CHOF%eINB}
zt0JDPy>PS(XVhfl7+V+a$JVB)_|-#pJCHO|qP+$UL9~GllhKzU)B!e1PM&oDc{`r*
zD)U813GzMiYu~`_baBv?{cKQ?SJ8LZqprn)JEq_>>0Il{?ssmG&edJijn?Qgo?8lV
zzwh$2Tu3X#&GlyQeD^a@9teZz^0=Z=B2~IzBX5yNRE=;th&eqjgIJVJ9=8!RgFxAn
zs8>PoWNivDUwM7tk{#+L0nf$LTxn)AE0IA;Axf={>0BCvX-LMn5K{?!Ex{_iG=SP@
zIz}6k?*ZT-fi?0V7V3H>&7esh+N5J`kT^&@aS&~wL7=pI)fkWT^EN95x!$Vowgs(x
zG;%Pb^hUF`n>R)xGnK*`&+=MF0+<$))NY7Lng0!#F_^!BgIQ(%#{PjnT14q%Ci92n
za&64Wv`j=s0<svngp9Oiz6R9gSW=Ff0G4*79ZC<cXG;~_?bCk{oe4vG(rp+SiOyX&
zHlk>6999`t-oSxAE)u2iUk3-JdW7R;CoAo(AVka~R^9@zmKhr_v9^Yo!aNP0a5Yk*
zZ^bBOMg)BQ12OR!MCaC1^Ie94k?2cNuS8!8(e=%Mwl*Qf%tDVGl)gu?)#$yVy=sI5
z)r|04rdI#-XXN0WS}`uibmTL!-5FCAkEo3k&{129JmJ{iJYjkpnU%L)H4|ZOY1<H<
zW=s&+4aK6uiu4@-^(?!IAc{p^-f3Qm-glyqoCMp+c?NK5?BGiVe9P@+3)^>H24Vy3
z-k$fuaH?Khz6W(B%<Bmvz#`QK0@?laZ4#j4%<`xd&rS&47>c<X^MzV9C_XtVVtwZE
zFR72Glh?;%I(`i2<o6e81L$b|k_Zir!63jC8fMW>9|R~3d?<i77}yvjhnH7kFwr*7
zSK@g$klj@rpz7TD0js#vI2emR`>*bVg09@@lR+8T<s%>|uDG|ZyFwt4ZKPNv@Dz5*
zbPosA2KRY&jm~J1?6zu>#spZak3?H#3p-EN-%8wh+ucPpF0RNWktsd_DiZpW0sNGK
zjf-oh;32eeolNmzAh$Ec$E`Usg<Zk4ixCWdAw7%+P(HW`t>Wd=1ifxt&T$4%_635z
z^`~BVKZYP`jSS*yl>;afFu^@#P;jW`;!xV4K9pP_!NBcs-L!KfIGL$`U3uIL3X=H?
z0sJDs7uNKjAT2h&EdAdIjCT6RkuKK1`|U`ZJOu(ff>SUtD?@RkET+B;tQjJ~)1*>(
zv6nC;Sl>yiIyp>A)6^Z?o4wVPVC0=)BrQ`P37je<Y$?LeW}eC<kqWqpQ;PaJNJ$0%
z8Ngcr?x@>kn>99mCcAtI813xxHEWLS!e_2Fk>PI+^{vGeh>4+Z0u)2H1`wxGePEFx
zvkHOlExJW!BgLY5c`Z|A&2QKM$CAA>>-Rm?O(u6EN$!7cVoxI{VuGZ{b9fr}814zc
z?+bc?vIJIY*Rcxhq~8WkPVjbsdL;M`z#g{V0r0d1R%AsJ@EjB*O$AWC#vjlK{Kms5
z9>tR3COz1|<UAC7!IC~S-r5{Kx+_(D3+?WS2%$VYK4HK6F#FWi5Eg-CWf0R|e3hf9
z<++sNPD~&%?*h0V1WLC8M1Rg_u4H%r3=;jaXfC=tc{ojBBYU1hi~Gi6Ia`=LBpBzM
z1Dc_p+n0!rBY3MmI^eW>0B;VIl~B)o$VnJ#?B{(+P=Sx0x*nVt<jtT2yBX7zeWXrb
zlf{3C*`$j90Vs?A2#q|PC1Jf!;AQy%3a0M@xm_^*z?!3Aihi1g0l{gVwE~aORlX;X
z=0V!@rvSy-&j8kqbZ8LeK=jW8sYqMury}S1WxxfJTM1@T+@ap^eMT^sMt%<B;^rQJ
zYP}bYhsH@K$b-QNw4T3MD*Fi<+NtbrYxcpex4sQy!{ehvEgu}L!eBgu4iNCKefi-O
zdoOEDxhts$H@j!|V9-JoC5jFdWN-;}&1AMO!C#<D()|*k*24P@$`9ucd-yi#?g<dy
z`O!eLlOLm+x1yXVaZhuc`USulLcx#-4~zNnf&T{pivJ<<@+%A&B0`WL`gEtX?)1)X
zl-N<_$J-f8KNQT5$F$iN^l9D_G0yik_Z*IDiD?*`=?aorfjYHAK07Lo(iJX*(iJs+
z_|UB}LpC@+*_aqB^+6UDfmSCrnc57jQ&F6x=PYtYuJTiW+Xsir9sqLmu@cQyq9;X%
znDnns+u6>asW~5)3oWYhr2PV}oeNPIcux{N8;5jJlQnuOp?*NI@kn81`diSD3+(_X
z7lMO07kb2?d>pd!Vm`(Cm_w)rdU&Tob)~mK{G2DdU?2CjDCCd47xxW|(3JNbjPf|Z
z_Rg+kr$>(9IdTLl4l7PR3F+i-pqp>7A~-Uh>*><@rivjM37b9pV%du9L6nh^s1<$K
z8q8iTWe;IU%f}9~($0*;2^c<wjm{58F%B^0Dl3iu(dtg)e*(xYcXp;het>Rm^26nE
z+kvF3K3ND=e|eLS3klp#NAezrdr*loS`JV8OXH;+W4?A$wSlsavR%qTpM4qR9v@{R
z%VXM0@(m@Sp!(F5{vM)G=}KO26x{=zh!{~3v5&6KCkJIvoAQTzp(G0^BEo8<rxR3{
zUjvM!XqTS$P(|D20$N&|?8xXOsCob?6pvI{1~zEEtYJ`oO<^UIN&YT^yP@@i-kI$=
z&GAt<8HX54TMbKYd4r}2lTi@O2vQ$;D*Q;}z`qG@&+Uome+G>=P<U?GB6Mc3H9$uK
z%|DIeMhM|@EBB+)7BQ4ZL;(D%QN|_z5H*_h-C@>9DCdgIhc2ve&lmfnJTKe;nfHOK
zq#(g6tQy=a>4+5ltb+{7T6=R8L{h@wZa3q%TE!tSrLuC%E}uBk07qMq&b6Y!0qF$>
zw(JM6OR>v>zkvVjGHQ)^912Q#Sj?V>3B>8_0Paih5G!-;jsly88;nLQEA+m9J7i2x
zMq|8%@fUbJGevi~)zwa=@Mbo|!Dfr){R4PhU*7M2C^pq<3~f>H%Y^<x+~O_om(5^}
z{N4!HCl(TB@i+~1049>yJe~-g8(QZD@IV9e`#20L%(qty6xqnG>O|`l20Y$vh2F}r
zHuMjoG2y;~E1DnR*rNNUD?F1Wk*&yogTWF>gAu}ZL1#sV*_i_}`%eVqybw%jVT!y7
z+ZywSV-#L0=8x1-3{O3e)_dGwlGcsnVxVw~#AA?xk{7T#y%e3|F*U4C`<p+;`U?qK
z;eP7EGzE?34@0GVXcR5|{4sqSa5Ek+qSMc#Xk82)=YIys^cJ`wi?$0x*C{9*H;7@!
zDY<!mRaYPfZXTVFuD4ndi)Xd`kL?66r%hFn&L0B}<%~d|+n7}_?ij6`T{VNs^)d~+
z=F?1Sjg+)N!YR^Lmf2`JVk}+<RJmWICD<k5?zu%vhoKpL!6A`t-2zt0Q0(10p>|B2
zI=>tP8g36oDH#AxO8RPP{TZGPa%=%-a&&a@-~fe513>_}V~YU5dfdA@xTgAZY=8K*
za<S*mbZ%Hw+s;(IGdsEXsH1=l@L$0HibK#Hgm7w$9SB&+%)GBFo(YI2{o>gM(tnG6
z&^XU8YWrKQ`UrW%-h`N9qqm!<nPTB)x}eVQjZ&&|3k;Uui{ckxHd}0k%beI~I`Aa{
z<if9fx&-}4aM()$h7T&;hv>XzpqD?0s8;60M=Jd;u~DalN%k&7%69}*d_dGM_Iul@
z9|>b-tLD=Z9?*YhMZ!E6UHAAr>U@uQtp-(sp|+kxH+}E6Rvax`)6?Zr3_!vlk^J`u
z85pi93Z8%UF$U=Ka08_#MWaTa#sN;ziDI`}sB$!L3gsYa?k*6CWwk0DcZR^jcnqP4
zI>HCP4r(Z#0YtcQdK;sUW-N~7Y;}_Y^|=3kV>0w)%)p{-NCim@sJp<9Ks}5>oHL6C
zidT^NnN?LBZ&+=eObPmU3LGuTh92c_XrkB$IDtc^VKP(fhwlAb?HCEr-#Sn|_0(8k
z$6a81SFE%mS>hAO-&tjP0;!H=ZT7_VEm{xgReNOZ*`dGumvGSRSad5FEDs=$;A(~L
z9Ky>0od;#xmd^gzJ`0OjhAijS6#6d{0lwoyGnW!~?(<SDv-V0Ve#vUT%-N-lCkWi<
zG9lqsG5PUcb|odGLM6*8Lv^y87{HSPh^?{PNUkOb;}sV+fq_NKtqFk2&`5bZ(Fmd4
zhFD9gdo{4G#)DRb*wYuBWXRtvWG5KLG_~x~VqpY|BccUD|KWgEbF2`>B~-~j8tC+(
zT^L(W4Xv*X;AueB3UNBXYh-gcW>Q>=vIKM)Ac?O)oI>kc(OSv(3ad<$Z&!R7B+o;!
zl?<P0pc6xxi>=(y$lhxL0+?#?-TNd5bUxj8f&5x@RJ`|FrQ#h2)LlO;fx`C4XSerY
z28HH901^N4FsL-$o8p{>Mu~HF07nA&>HxmRz<fK0jS__W#x4k-&E{LdX^Lb0h72Ao
z6YegL_b7^9eR<3P=tB=aqUj&AgI_ml*dk<C5!C$&*JpYGZll~OiK~Ci3x*Pj;lq7~
z|Lrt?cQ#$yyA%pgG|4k?t8J4_S{#YuvsBYM1D$p!0=PbalL6cS)bDT@osfH_SR$`Y
zOv}(npNG*>>3aYUg``oU&ZI&4@!x}(O2zSGb!8HT%A}*qdSCbHbgfaEuC2c)us%oe
zHiI|$+=T&TK&W*~Xnh?}+bjyhKndRLE{jY`wo`igQWaqrSVtv=-UsbNll~$5UlAup
z2JOfFSRj^iv|UX?W}CQ~-Ej$_o*w+8VDh(q@<!gLa4J2;v2Hh(?$!~*__&u{1W<Q*
z7Xy^2B;PaN>e-oS+|jgBH;=Obo#8|(b|7+ehrrpU0^*dPjbbl>b+wU3!jvR^;J@}u
zhT;k99#cQBSNKDS;t9jV3ylOQ!CH!?S$kLP==C48;b*d_6pwgZ?ZD|m@TlU6z#{hT
z`q^mspALEhPh=bkAidS7E;7JIvm3smfyBAUJLMbE&bN$qwhT|dyKc)lm_69Gz%f+M
z6WJ92Wx^`~%7kwR*hBMdWvdlUxIys<pl7w~*}-n;Hh-oSwzQ$-Y6<H$_iU{fzx6sM
zWBR~bjPjj1gF1`~3hcfTJxbl~>&3%fZ<kwBi{7x<gdm7xz`4FXC*H9Qgp!$qU^co}
zp->R8jy+KEFa*i2MVA!!4uE|4(GN0$?>FbuUpiRs4YU)xQ8IU*0my${*_;o}We=bY
zy9Pvw+*LmH5ZZ#L+7A}v-Up}k(vO=5S7?E{h_L=p9A){W5mBf}-$ViB=HJ$Oyyma5
z_Lg^@R?R={^mCBW(fzW8x8#zyQt5Po$OydPa_BZNnV>yB08sY$AV4|thX6+QKsIb5
zhoHT=^k6IXdRAozy~1$fULfh0(-k8PF4eZMU_oP2(Q8?AdC)K)UBsZB`y~&SseH1>
zN`6ny%;SD^j)8jj15%TT$vv}KJ;wBWN3VY1vGHh7AnMKII1ily%A1MjWK}dZl&ENR
zFVCopYe0HhqkEQCO>b=#rMUt~v{bb`y&rh-+ia_MJne)Qglp#=QEr2gnn!^VzTRh_
z0w|Zb5ujY+CV=(aHf(K8u-`nZmfP4Px6%9Hw=kZfHlc~;k>12~S$&Qj=P{^ZS{@S`
z;;ea;kETyrtwmogYx&boV>7A?`8&>NsPmn)c@&JFeGdIn*XIE$qumTJilFnY+PuJf
z;`uX15NA`a0Y?eyeDa>j8=J4A=CRhMKR|J-#szs=f+@YzaO8H_=AF0Dsy2{rxuqJT
z%cs?qpSwD6<*X5=vm;UL2kl045oyZRv1&KpgyND`YRzrH5;d=u3o22Z$kjC5)iqy_
zAz+(aHy#OEgiGZc0(wc)d<pn^%ca$js@;G0<TFutx1Wso!)QjeyYlAfldX;FbFcYZ
zte$h*+JPSXZw|FzY5XqY%X>K(<kZcp0acl>nm<_*&2Jb@u9Qk>-1@+{ZaVM!pS7km
nUAfl&uXXq3lq&YsS0czhpcY_B#6ctOL(=q^v7u%7KjQxnTxD7X

diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index e7d957a0b..18ee9fecc 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/src/library/simplifier/ceq.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/expr_pair.h"
 #include "library/ite.h"
 #include "library/kernel_bindings.h"
-#include "library/eq_heq.h"
 
 namespace lean {
 static name g_Hc("Hc"); // auxiliary name for if-then-else
@@ -45,11 +44,11 @@ class to_ceqs_fn {
     }
 
     list<expr_pair> apply(expr const & e, expr const & H) {
-        if (is_eq(e) || is_heq(e)) {
+        if (is_eq(e)) {
             return mk_singleton(e, H);
         } else if (is_not(e)) {
             expr a     = arg(e, 1);
-            expr new_e = mk_heq(a, False);
+            expr new_e = mk_eq(Bool, a, False);
             expr new_H = mk_eqf_intro_th(a, H);
             return mk_singleton(new_e, new_H);
         } else if (is_and(e)) {
@@ -93,7 +92,7 @@ class to_ceqs_fn {
                 });
             return append(new_then_ceqs, new_else_ceqs);
         } else {
-            return mk_singleton(mk_heq(e, True), mk_eqt_intro_th(e, H));
+            return mk_singleton(mk_eq(Bool, e, True), mk_eqt_intro_th(e, H));
         }
     }
 public:
@@ -118,10 +117,10 @@ bool is_ceq(ro_environment const & env, expr e) {
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e = abst_body(e);
     }
-    if (is_eq_heq(e)) {
-        auto lhs_rhs = eq_heq_args(e);
+    if (is_eq(e)) {
+        expr lhs = arg(e, 2);
         // traverse lhs, and mark all variables that occur there in is_lhs.
-        for_each(lhs_rhs.first, [&](expr const & e, unsigned offset) {
+        for_each(lhs, [&](expr const & e, unsigned offset) {
                 if (is_var(e)) {
                     unsigned vidx = var_idx(e);
                     if (vidx >= offset) {