From d4a7d796a5cb4e02b33cdaccf7c2900c4e629a85 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jan 2014 15:20:55 -0800
Subject: [PATCH] feat(builtin): prove strong induction theorem, add < theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/Nat.lean            | 142 ++++++++++++++++++++++++++++----
 src/builtin/kernel.lean         |   4 +
 src/builtin/obj/Nat.olean       | Bin 15355 -> 22089 bytes
 src/builtin/obj/kernel.olean    | Bin 15446 -> 15524 bytes
 src/kernel/kernel_decls.cpp     |   1 +
 src/kernel/kernel_decls.h       |   3 +
 src/library/arith/Nat_decls.cpp |  15 +++-
 src/library/arith/Nat_decls.h   |  45 +++++++++-
 8 files changed, 188 insertions(+), 22 deletions(-)

diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index f090586be..e943b6d64 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -21,10 +21,10 @@ definition ge (a b : Nat) := b ≤ a
 infix 50 >= : ge
 infix 50 ≥  : ge
 
-definition lt (a b : Nat) := ¬ (a ≥ b)
+definition lt (a b : Nat) := a + 1 ≤ b
 infix 50 <  : lt
 
-definition gt (a b : Nat) := ¬ (a ≤ b)
+definition gt (a b : Nat) := b < a
 infix 50 >  : gt
 
 definition id (a : Nat) := a
@@ -37,10 +37,13 @@ axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
 axiom mul_zeror (a : Nat)    : a * 0 = 0
 axiom mul_succr (a b : Nat)  : a * (b + 1) = a * b + a
 axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b
-axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
+axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
+
+theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
+:= induction H1 H2 a
 
 theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
-:= induction a
+:= induction_on a
     (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H)
     (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
        or_elim (em (n = 0))
@@ -56,14 +59,14 @@ theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n +
                   H2 w (symm Hw))
 
 theorem add_zerol (a : Nat) : 0 + a = a
-:= induction a
+:= induction_on a
     (have 0 + 0 = 0 : trivial)
     (λ (n : Nat) (iH : 0 + n = n),
         calc  0 + (n + 1)  =  (0 + n) + 1   :  add_succr 0 n
                     ...    =  n + 1         :  { iH })
 
 theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
-:= induction b
+:= induction_on b
     (calc (a + 1) + 0   =  a + 1        :  add_zeror (a + 1)
                   ...   =  (a + 0) + 1  :  { symm (add_zeror a) })
     (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
@@ -72,7 +75,7 @@ theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
                               ...  =   (a + (n + 1)) + 1  :  { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) })
 
 theorem add_comm (a b : Nat) : a + b = b + a
-:= induction b
+:= induction_on b
     (calc a + 0   = a     : add_zeror a
             ...   = 0 + a : symm (add_zerol a))
     (λ (n : Nat) (iH : a + n = n + a),
@@ -81,7 +84,7 @@ theorem add_comm (a b : Nat) : a + b = b + a
                        ...   =   (n + 1) + a : symm (add_succl n a))
 
 theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
-:= induction a
+:= induction_on a
     (calc 0 + (b + c)  =  b + c        : add_zerol (b + c)
                   ...  =  (0 + b) + c  : { symm (add_zerol b) })
     (λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
@@ -91,7 +94,7 @@ theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
                           ...    =    ((n + 1) + b) + c   :  { have (n + b) + 1 = (n + 1) + b :  symm (add_succl n b) })
 
 theorem mul_zerol (a : Nat) : 0 * a = 0
-:= induction a
+:= induction_on a
     (have 0 * 0 = 0 : trivial)
     (λ (n : Nat) (iH : 0 * n = 0),
         calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
@@ -99,7 +102,7 @@ theorem mul_zerol (a : Nat) : 0 * a = 0
                       ...  =  0           : trivial)
 
 theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
-:= induction b
+:= induction_on b
     (calc (a + 1) * 0   =  0         : mul_zeror (a + 1)
                    ...  =  a * 0     : symm (mul_zeror a)
                    ...  =  a * 0 + 0 : symm (add_zeror (a * 0)))
@@ -114,21 +117,21 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
                             ...   = a * (n + 1) + (n + 1)     :  symm (add_assoc (a * (n + 1)) n 1))
 
 theorem mul_onel (a : Nat) : 1 * a = a
-:= induction a
+:= induction_on a
     (have 1 * 0 = 0 : trivial)
     (λ (n : Nat) (iH : 1 * n = n),
         calc  1 * (n + 1)  =  1 * n + 1 :  mul_succr 1 n
                       ...  =  n + 1     : { iH })
 
 theorem mul_oner (a : Nat) : a * 1 = a
-:= induction a
+:= induction_on a
     (have 0 * 1 = 0 : trivial)
     (λ (n : Nat) (iH : n * 1 = n),
         calc  (n + 1) * 1  =  n * 1 + 1 : mul_succl n 1
                       ...  =  n + 1     : { iH })
 
 theorem mul_comm (a b : Nat) : a * b = b * a
-:= induction b
+:= induction_on b
     (calc a * 0  = 0      : mul_zeror a
             ...  = 0 * a  : symm (mul_zerol a))
     (λ (n : Nat) (iH : a * n = n * a),
@@ -137,7 +140,7 @@ theorem mul_comm (a b : Nat) : a * b = b * a
                        ...   =   (n + 1) * a : symm (mul_succl n a))
 
 theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c
-:= induction a
+:= induction_on a
     (calc 0 * (b + c)   = 0              : mul_zerol (b + c)
                   ...   = 0 + 0          : trivial
                   ...   = 0 * b + 0      : { symm (mul_zerol b) }
@@ -160,7 +163,7 @@ theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c
                 ...  =  a * c + b * c  :  { mul_comm c b }
 
 theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c
-:= induction a
+:= induction_on a
     (calc  0 * (b * c)    =  0           : mul_zerol (b * c)
                    ...    =  0 * c       : symm (mul_zerol c)
                    ...    =  (0 * b) * c : { symm (mul_zerol b) })
@@ -170,8 +173,8 @@ theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c
                             ...    =   (n * b + b) * c         :  symm (distributel (n * b) b c)
                             ...    =   (n + 1) * b * c         :  { symm (mul_succl n b) })
 
-theorem add_inj {a b c : Nat} : a + b = a + c → b = c
-:= induction a
+theorem add_injr {a b c : Nat} : a + b = a + c → b = c
+:= induction_on a
     (λ H : 0 + b = 0 + c,
         calc b   =  0 + b   : symm (add_zerol b)
            ...   =  0 + c   : H
@@ -188,6 +191,11 @@ theorem add_inj {a b c : Nat} : a + b = a + c → b = c
            L2 : n + b = n + c := succ_inj L1
        in iH L2)
 
+theorem add_injl {a b c : Nat} (H : a + b = c + b) : a = c
+:= add_injr (calc b + a  =  a + b  : add_comm _ _
+                   ...   =  c + b  : H
+                   ...   =  b + c  : add_comm _ _)
+
 theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0
 := discriminate
      (λ H1 : a = 0, H1)
@@ -228,7 +236,7 @@ theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
 := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
    obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2),
     let L1 : w1 + w2 = 0
-           := add_inj (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 }
+           := add_injr (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 }
                                        ... = b + w2        : { Hw1 }
                                        ... = a             : Hw2
                                        ... = a + 0         : symm (add_zeror a)),
@@ -237,6 +245,104 @@ theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
           ...  =  a  + w1 : { symm L2 }
           ...  =  b       : Hw1
 
+theorem not_lt_0 (a : Nat) : ¬ a < 0
+:= not_intro (λ H : a + 1 ≤ 0,
+               obtain (w : Nat) (Hw1 : a + 1 + w = 0), from (le_elim H),
+                  absurd
+                    (calc a + w + 1  =  a + (w + 1)  : symm (add_assoc _ _ _)
+                                ...  =  a + (1 + w)  : { add_comm _ _ }
+                                ...  =  a + 1 + w    : add_assoc _ _ _
+                                ...  =  0            : Hw1)
+                    (succ_nz (a + w)))
+
+theorem lt_intro {a b c : Nat} (H : a + 1 + c = b) : a < b
+:= le_intro H
+
+theorem lt_elim {a b : Nat} (H : a < b) : ∃ x, a + 1 + x = b
+:= le_elim H
+
+theorem lt_le {a b : Nat} (H : a < b) : a ≤ b
+:= obtain (w : Nat) (Hw : a + 1 + w = b), from (le_elim H),
+     le_intro (calc a + (1 + w) =  a + 1 + w  :  add_assoc _ _ _
+                            ... =  b          : Hw)
+
+theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b
+:= not_intro (λ H1 : a = b,
+      obtain (w : Nat) (Hw : a + 1 + w = b), from (lt_elim H),
+          absurd (calc w + 1 = 1 + w     : add_comm _ _
+                        ...  = 0         :
+                               add_injr (calc b + (1 + w)  = b + 1 + w   : add_assoc b 1 w
+                                                    ...    = a + 1 + w   : { symm H1 }
+                                                    ...    =  b          : Hw
+                                                    ...    =  b + 0      : symm (add_zeror b)))
+                 (succ_nz w))
+
+theorem lt_nrefl (a : Nat) : ¬ a < a
+:= not_intro (λ H : a < a,
+      absurd (refl a) (lt_ne H))
+
+theorem lt_trans {a b c : Nat} (H1 : a < b) (H2 : b < c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
+      lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2))   : { symm (add_assoc w1 1 w2) }
+                                       ... = (a + 1 + w1) + (1 + w2)   : add_assoc _ _ _
+                                       ... =  b + (1 + w2)             :  { Hw1 }
+                                       ... =  b + 1 + w2               : add_assoc _ _ _
+                                       ... =  c                        :  Hw2)
+
+theorem lt_le_trans {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
+      lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2   : add_assoc _ _ _
+                                   ... =  b + w2             :  { Hw1 }
+                                   ... =  c                  :  Hw2)
+
+theorem le_lt_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b < c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
+      lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2   : add_assoc _ _ _
+                                   ... = a + (1 + w1) + w2 : { symm (add_assoc a 1 w1) }
+                                   ... = a + (w1 + 1) + w2 : { add_comm 1 w1 }
+                                   ... = a + w1 + 1 + w2   : { add_assoc a w1 1 }
+                                   ... = b + 1 + w2        : { Hw1 }
+                                   ... = c                 : Hw2)
+
+theorem ne_lt_succ {a b : Nat} (H1 : a ≠ b) (H2 : a < b + 1) : a < b
+:= obtain (w : Nat) (Hw : a + 1 + w = b + 1), from (lt_elim H2),
+     let L : a + w = b := add_injl (calc a + w + 1  =  a + (w + 1)  : symm (add_assoc _ _ _)
+                                                ... =  a + (1 + w)  : { add_comm _ _ }
+                                                ... =  a + 1 + w    : add_assoc _ _ _
+                                                ... =  b + 1        : Hw)
+     in discriminate (λ Hz : w = 0, absurd_elim (a < b) (calc a   = a + 0  : symm (add_zeror _)
+                                                              ... = a + w  : { symm Hz }
+                                                              ... = b      : L)
+                                                         H1)
+                     (λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p =  a + (1 + p)   : symm (add_assoc _ _ _)
+                                                                        ...  =  a + (p + 1)   : { add_comm _ _ }
+                                                                        ...  =  a + w         : { symm Hp }
+                                                                        ...  =  b             : L))
+
+theorem strong_induction {P : Nat → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a
+:= λ a,
+    let stronger : P a ∧ ∀ m, m < a → P m :=
+      -- we prove a stronger result by regular induction on a
+      induction_on a
+        (have P 0 ∧ ∀ m, m < 0 → P m :
+            let c2 : ∀ m, m < 0 → P m := λ (m : Nat) (Hlt : m < 0), absurd_elim (P m) Hlt (not_lt_0 m),
+                c1 : P 0                := H 0 c2
+            in and_intro c1 c2)
+        (λ (n : Nat) (iH : P n ∧ ∀ m, m < n → P m),
+            have P (n + 1) ∧ ∀ m, m < n + 1 → P m :
+              let iH1 : P n                    := and_eliml iH,
+                  iH2 : ∀ m, m < n → P m     := and_elimr iH,
+                  c2  : ∀ m, m < n + 1 → P m := λ (m : Nat) (Hlt : m < n + 1),
+                                                    or_elim (em (m = n))
+                                                      (λ Heq : m = n, subst iH1 (symm Heq))
+                                                      (λ Hne : m ≠ n, iH2 m (ne_lt_succ Hne Hlt)),
+                  c1  : P (n + 1)              := H (n + 1) c2
+              in and_intro c1 c2)
+    in and_eliml stronger
+
 set_opaque add true
 set_opaque mul true
 set_opaque le true
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 1b3e0c177..3db5e8a5b 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -64,6 +64,10 @@ axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀
 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
 := funext (λ x : A, refl (f x))
 
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index afbe1a8d74b84e4a5bacd2085dad57fd3217a073..aa07bb8c14cb57ff319e7dca287c8a4c762d0c4e 100644
GIT binary patch
literal 22089
zcmb7Mdyrm5mA~D$?_`2ALJ}THAP^R2pkRfBT8y<D0t6=s1Y82LfC}Se@+AyRW|Emn
z2#?eb_z^X$ybLM|_*}qpVKJ~`aOGtT0oh&mQMHSpAX2q|NRYyH-9=sZ{C?+txBK>Y
zzb`|IYEE~bK7IPU`gGr(Z*;geFtT=NxR&Jq%+UG`qhk}vRkg8^+HkUYU@Wm87??<=
znZ&Lhok#|ThX%$I`)d7;#OjdMn}&ubhDOF~6G=KEm<y7;h1LFnHEWU&j7|(p42_Op
zfUzfX<eAoyF#5|Q)^8e)Mx4MA%kmNEFOLxR%Tp{qEip3JDftL2uZ-~OC%>*3V5xIW
zZEd35tg9s*b^wiu>9DI6uy*O_sLYw6dLRlz@F0T6qU^+Uq-e?$EopFq{&zQV@z<V<
z8RP<J-NO_3U-GW3!AjO(MJHqFfYMEoF9eu$m1ka@ivV2*C!YAa_QVe(DHPphdP@R&
zvjciVYrM!XOl32VAc_)O)?S~;f77IW5$)%QWME68OBvrZIM_dOt*6#w?MQ7SXb4rm
z<}TD{qOj$$LnBxE!G-oZ?21Gv6@)Nw7K-^jD33v5pg!``efIhdXkoiGrkFwOwEx=L
z*yxy_A{ZZWM^as-u~=O&wqUQ4NH;i`uS7j*w(9B&(&7yJW2*ziIE-w0p<(P)*&>l9
zwtOq;cNc68*ZN^`&A#N9JDm&b1arEuV?{|@hQ=qx(F8lPg9`XDffcYZnssPo&89&H
znhtwD#~vWsU#L1(2}u1EVT+*%E<UtEdzIWVu!9sMXBDi|K$fGet6>|9q+-m(6}jOS
z)Amb<3uZ3jNP`8g(^jwm>MJ?9131gi*^{B+bQA{=JOiNm*qH#&XX{dcAMB-q7bTh9
zf_h>|XB9w|Q~~ugma+tBekmKqYHLb92r*DLM`0|)lbaH?cN!au=tM-$NyPc+)df&~
zM)_N!fwYffQLIJLmBCK|`I*#S#V*zk43F3PYr{k9lVqwBbFfg&Rh>cA__wxVBE|!I
zytSia`7F^=ShdGUK$1O>|HeZ;&~h#c6OGG#7+n;>Od(N|Md07KFjCvNK;hno@%Imn
zOpJ}PF<0~c2vffr4`l`8n^uqKEK&&+!}1IS`%supGVTDgk0a-ckjH9khtZm=`37NW
z{F?PSv!ul(G~~Ksq_!Ydn2PDRVlApMl5A@vs{&yH`!7)}%k0(oKO(^jg+ASj`t{m~
zvYl+eG6NJ>IO}-ePom&jW}(cQ<>IBo#c*scB8;u02*MC8hy6u#SOyI5Qfr3B2gioi
z4@qu><YFlZB-4xV!T?oxnRlKppi$O6alptu(&LiT`4~W3P;Fn1`gAU^AE3sJj{>}(
zt*ZfklVTYI$hf-+5cParXr5>leNg9s|LQoDpF%-t-VA8fvE&!)&uNJJHK~vS<_z7`
z<~CrfN&xLZQONQ#smLx|gxba~JS>tN0A|VKyza;dMcBo)UP)BWcLf{z*nr{*6kXHp
z6$6_k#BA9x){Z3UT5Bi9hBglk3}YxmR~%%X5Ko*K8yIQqWf5nyv>vr`d!Q}NQc0db
z@|?3fGT*)E>JFBYyLCje2WU;^i^gYBbd>~)Tp$o^`xJ$SPYIt)E|{mOjnSG+ldyxp
za|b8)ykZwpHoLgaJ*dZCMmaP|jzVLX#8wO=fh2Z!qP-Hz3%KM%V{{#LHA8Z~t*E~O
zsGHvQD#7xeLJ@mkd=V%wRjy()x=IW15>ST#0<|?$d!l{~HUVwmzaFD<8gEO#WdCzO
z)gF$YM4iih3(y;(WMYC_fx%@~TGFr3t$LdTNUCoDdb1T(zb*zWPrGu0Urq<HtKz*?
zr-+pGCQ#q-OZIXt+xp<B>}*90sWNpCI>|FiQ&)$h7}eAn-6~8SgO@~uxysPKf%FOr
zDr+yG|BRNy#%?w2As~p)mogd>_14F9ZboDwZz?069nMF|<aP$aG_K|GQ1n31W-f}9
z-ID^UmiGae6KWY<zef>!6}8n>UY<Ez5Y1c-c6#hm)=FV%V0?UZutHZI`#&G#`tvKN
zxHyOI3)g{FRb`M>(BLby>gm85%!x(a%m5wI?Fl4U^y@}`5|9Fu+KYM@lxGeGcv2)?
z(%TzJ*PICaZj!EJ6x|J^&7ti~!z={KDV5yiF$vUY6+H#xRC^NCp|K=fqg2i5itk6w
zAr=Zav^gV~74;aOk~767V9o+1bF>tBPgyYL{pemA3MOJ8;5bi-K&vXam_GExc6o-h
z1zZ?iPs9a1;_y~n6vEKR$v8&_mir#Y6s_0622^RzsEl^%fAkl6yN_m#8-QTv?g23k
z3Y@G1b#9KF(URvI(AaF`Xk3G?u4X<WVx-7oHwTo>kAwonM}rw|p2j#EAYssz#B>op
zoq>}*t?}YyjMY^|$&tB=JuNijg+Vcq<O!Utj$zcnFd)imcM*yjw<Up`tF{f#Hdoli
zx&ysMBucJs0;pkU8$rg!Ff-L;iM)o%lBZ7Q$)Xm45IquEu)eNBWZi)SP9Dpj%t0(>
zn{GVs0gK5j^2iaCk&b2b`ULu;Y~Fla+JpkSUL{yI5Av@zirz^SH&!m9McULMBQ#ub
zm0X(N&dlxT)+}%jK=OQ>F1@Mrv`B_QPzhq>j({!HOH|PCSt*izC>ZYUoC?0i6ykre
z9llo<XYu@T=-t&rg%fiR_<`)qm#dLTnJcG+NtyUxL62GA7@x%M^;LA=lcB#4MdM1r
z6Z9G5)`EZaC#}~x3`4&LsH=xwcr9DWw<ag#dy=hEm@lEYtHrz;FM_DyGs_-O@Bui=
zOw5;?1D&6(7h|`fpaI<l;7cHA9zYT4B+7zS$NO4w3<3|KxIl^|PWjoTLenlUw7WF|
z@~o~|hvsdQphG^t0O0fcn>hI$2EdTwbj^G*TBEu|q>#_aKy!PmSqjbTO1wS-FP(w8
z<K^8M3H^3V^Er@Hqf}lZBt%KG!*h*6Dw~<55I%~}T1Day{HC3f0@0|-wQUDd^-lR3
zy4voPBu4XQv6}<Rp%Bzx3w)G<>i{ALhbKngN_X}BDjC*ecl`w@wYn<s1Stv<h#lm0
z5GW@cBE{fiMx_)fK+@Ax`({w7mg3u-pxF(*ASgQ$Yb(XKE2YT&A#^V;+6$0$^DCD+
zSjp|CZ0#0~)n1NXgjI61WW6lMsU1TXc|lOBs?6KLk0ueHA=rzultcjGhG;OEjE<ps
zA^>#cPG&nvZ4*$#i6&H<4NRi7{V~+sAQ<-GKp9dux08_|LQ?~DX3c@A7Ah+`hH^7E
zh&FZ}DE)g`GmOIah)lW~8xpX7r1PPbQqxQ3I_iv(pciNU_DE^7^Dxq;=vN+#2qKrc
za`m@*(?n?gMH<-hM9P&>@ZpKnw_+A^0~bK9RI8r{0}9?ruoq=X!CWHgV2Qzr)Z#>G
z55j=(wC3??j660Dv(aHZl|NY4n|&XMJdN(*svZ)08kw9u446FS?k;PHX}Y;8(h!Lz
zQSQw~JEv;=U^L!r@SO9D31u)&DQyEQRP!Jp>-md52~jKPCAR$&AfFnn(@PANY5b**
zJyK`)2(%T_^9SY}iz=dNhuXkgX9rXq8fby%2$X=7JvZP5^(K6Hg!TC6?+^b7olr(G
zdk%(PF!iB2ioQ!OFKRcmn9v?k@al(NQau!ymrB8F0sG-<BvPhq=|M{h{Ewi=d$3u;
z@srZ1YQ7BJmu9H<p=eHFu`B~FO>|(->vay3!d?!ji}(+q4zBZilxWruq5I+%vo<BL
zpeWx|P;!Z^Q*KP9$lFEi_Pl(!7wFqi!1(ROC_dzQ3ltFX_7}jsuoZ9U%+KWjxgRJO
zWFY6ASW;-bjV?CqB|tU1fkbnSa#s66^sJg12TbRcjY>IOR9<p!>CuwuIY+jdP!|TC
zu9PC2Fj_KKoAbi1I`Ap}3k0yekxtG<<N2P!z~LhXR|50A77WrRcsHOn;($!Wc!RaN
z$3<M78!>bqMy>>s_n4%oV$TZ_=c(;^ysS+89S9SHWD!?%x6GICZufW)XS~Ev4toen
zVejVxut3c$u&vo|#7Jm76~%*9JsQ~c;B=c{$!3W%KYH>Ur)CSq#7AE4ruhclhkny3
zg}t=kOKspB*6Tz-|EZ|kzeSxHh{pa&)M*~vo>dw-)q<erG)m9`pB$<r{R9t26Lc3!
z!)?_&zBs2zas58ywA{}%h5rgU&rp8VgI^;^n`)DrSj~Je1*NH(Rk#~+?PP%|#UjBp
zgGHlW>P300{SoE{x*7C4JVx3+8o{K1ly!9mLZbE{PEv26nn8i=obnlsQt@fR^FaBB
zz|IOj^ACJn2ZOcd0$eu&PJT7bIy}FWo=MfdNK!sc=BBB+z>m=%ep{@<r(i8nS-cE-
z-m&eE%Yw15p!=s(YM+2rTcKZEvGdrUE1MVr+s^BC)M?v40~Fn>+n1!xzO1)BcL6~c
zr*ew;Y7w0&xa}Al92)3d@qWX}dJB)h(*b!Q7#v%hV_5S$42=>?FkdfabRR%X%J28!
zHwgBk41GXeZcuai6@&EhOOfgB1g0(<kUo<7W)I-P$dbLNK2EXh0SLJ&Iriu|Kk9*D
zCVR=qHh>(%#vTyX4^5m0GBbyitvtUMNo~Z5aw_jX;?*4Ptw6Ke>Gs@(r3Vz4<wC{s
zxFk=aGt0|spvownYO?@o^g*+P<cadk4Wem$?VHaJqTDcvbV%!&byo$YLt7*H9AB?#
z;2P;+ZSXPuRv^tOt0$c+jpjnggqMoCaC(|bXHt4pksLldL%olU!J7)d>+2gDf6JzZ
z7VRDBTu6@TSbjGeF+g#Wi^z-9Lu6ojXcc;t(xo_rCYxLE3o5fw97P@0feUj@5AmF-
zPNS*RaKzG1DOnn+I8Y(Nj;Ov$!w%gmMV^qp7q|=^D;v)t??t<b9vn&3Xq)*|csX(l
z(+$1@e<oXcck?iM3<dLu2mj84-xe@EOCL;vsoWiuMA^tv-M_f<;s|O^jFE%{&r&Iq
z3ROHABu!d}HY$yVM0U!!CW+KG2G6vEFdD}Py$s-XKF-B{2P@Ha@ABYdm?M9^dRfwm
z4synUJrZ^nqDdd9g~xYkC!P<PT+4iUxj3+TeAC#P%Ez2M)g^I=qowPF@^-7Xv45o2
zAHLv{`SmymZ*BT!88{!shp=VlmQ@fQB!NWlNIx1QVI;ourUUGm6i}U?9L}N```8#b
z{|+<&!A8!ci;X>aKrqeWkex;x@~pmAp0vV)Wl%atiu`>`9U$EnMAHQkQ7R;VnKhrN
za~hWQs8qwZeez~p-@X>N^MPdzVk{nPuOOf=2s#0C2HilPLS3!vX%BwigS!Eqj<>cO
z@ywqQ;xymQfDk@2B7y?~h0j=l`O@or2*<T`igzSwT~8OM2;5*Rztd(fhg^?7itA&5
zD0q@Bo;*G&%_WBux$qrrl~`07i^GL9-hM+7KKP_Zp{inf2B3;*uLqw6xEM^PlcY!K
zk_xSrUp>>CfK@d5hnjn&IZ`Iy6BkT-lDgasgq}xXG|D{*Si><fcxA^=$HBJ;kp=z;
z!+*f>Wa+zlPWeYr;-`l6Zh+baD0pq-FXDx$dV0ZZrQt0Ef%Fc(#wFzErgf-rc_LBa
z{xb$B_%9y(SB~ZK|Bc{r==&53#eI$-WvqdX^EkB9%_$u{^G`#gPOiHf)R4EpPH|0t
zHTf3W@`##X`oKGw@m5gbjJlt4MmDYjhv`G;FQShan7vx<pYst+AEr^=4XdY3arnOD
zF_QfHhn^{7Lb6X6417*UC%HAimyYy1id4u(hw7ry{}|X~bPIb(WKw$62fr&ox{JE#
zV`CmtJp*)Ll`sa)U{9U682k5tFq8L$f09b<zxX4!D&ty#k;&rXy8)?pf&krh2|2?l
zE;o%AJ&4myvX}@zVQZjNsiz+!EyypY1uj)x6cU++d0?<w2Y~cORTf7(v{1Rk{vE2}
zsiQzj$)i3>^LK$dl-kqrkqYyZZex-Zw}R<U+9UBimi`n>`fJYgWsH0gljwftc~*8O
zrH2~V;pb$i_pve9L}8bjBJJeL>O_zt<rz9inV8uHQ|TJX`D8JO8ftf+na~j^8mPoX
zm$@nRTI>ri2uc)T2Sz4_<WDrJO-tQgY)k&&iOYdq<+m;Zq#7!JhDMD$uX^z30M)o&
z6DWN<HZC-#C|;-vFgFJ16m?Tb!_dExBDs}ZX#jyF)I#ZSs>G^*@`tKZrar*2G~cs9
zi3#RDOcK6uq9|OcKiw5IhWLW%0+Xi7pzd^6*-#ru5h?l_@LfmQJREp%ofJ=>fW^Iw
zfEuyrZqcdDIS5I^8rP@vBhu4A@78A0o;SwXmSN3NDVQm~!Eqp(?&7`#dr5ccF%014
zx&@JRz9~s_{xVzxJ<uNaTs)3`s5yPKEX*b(?BH%*+3Ovy&(g;|FM3rnDXsK%-S&4h
zivb(U0l?Ciaa6?7sK>%SvOJ;2GoMVXYGksnfL3s5ls^*dAD-x6;2o1pPH^RiaV8X&
zti2A<$lqUKRQ|_bM5Getqu1i*MgF-zn~Gy4+$H3XRQOkOx;?2|@rp+IF9m*v3b$DP
zN>-0e`9A#y=Pql8kHM3-DtijW=2vqNtlo_<KE72&=}kd#XGL;GWAX;<Ph)K1L`i%h
zf)%-?%_;@~nm4X;QhfqZM<aBfya`T&!|u#zs+m9{&&(Ioji~P{ZW2YcQ#z=Cs?Wex
zExJe22DmCs8vhHJ8ijxD!T<K)Zv=FgKuns^;(V!jhqBqQ#9sj;yuT1$+Z-OKF*2iM
zSkDhc73T<cJ50^_nHK5-{uhn9fVVyPTLIl5#E?G3vDh+{?Lfp0-v3AXLN5~5<q!8;
zrcG`Tbnl?<{||I^`acvPRqY1%>oU43&mZ+d{&a!tnFg{{C?w^EOa6mCSM%DT<$;V_
z8rZzf16=gGrM|uujnu$$Orb_kA{Ao#y<kLQ8fhyga?N~_646Cun8!(>VpG|%G#%3D
z_~FI<DG+*#3z*(mmfWJM56oN>1xP_G(aixmZk&w)H7B6%6JXGt(TQ#iSb+>1jczF*
z?h5Bn?%45jxw5A`#%*D@mpFwRZ}VG<{&XJjsgYF`l-xDa>uyGIExRWL)X+l06?=~K
zE79QEcs@pHy$%rSao1ouKDE_7hg7M!=qAT~8rZ9fJy1anSdE`DFz~wAV#<eej*qt|
zCWz);n1ClVT7$c<u@~JJ=!uew|0boID(CFEEQuDJyC<f2?xtQCrYM8%#u40Up3WW>
zQ3ht;O_m8B=)r?LI72|UlL&Ayw{z-ttxBX_=SOfd2NCOrLyzqNpKg262p6b4i@V3B
zK6P>%sBr51EbgafTFR+;EZ3<utHz+JW4U`$?_IEE<QXTagxfSH@Y%2CrJUxixQp2+
zyQt;pxbB`&d`tyQ`mcL7@~s@HKy`b-8{-H3-91;0k1k-kvrs%AdE{H{fwIddzG9Y?
zX((C$b<yZ}hZHA-&y<~$6EYcc=RxBP+#%CtR@@H-r}cG%bn2{XSWfDiJp~~H+IKII
z%R2fQGM)!SlM4<8UKNcKq=91M<lvp$eYu?t$4ik`xrgaNvoX8w9CJK4*Mo-(n0wn1
z0;YEaCXcS~qWB()$14t#B@e;yM}YZ#K;N!98}hQr{Q&)sN}*@$%F8BI)IMN7M$E{%
z0%L&UxE%!7N?y<LYmt_E79#FHK#Il^-6c7ud*~_dk_;kSSz|REEZ)Iwr4VqBP)~mZ
z%Bm-Zdj)Aq3Sw%>r*K~&|4Km-JrAN0YD&LVp{CNMA~2sq0X4bZ6>5^;gRUP)(Lzn=
zMlS4lFCB-ITsP$2fe4JqpEa5yOA|hAgIO%RB0H#B_ntoR^<xO}^&G<RL>DBdP+)ej
z6z(?_j-T<Yg6!D+wj4&Z=ZBELIxv}|15fpXs%I3zjGt8-e*;<W()}Y!I>>aopv-iJ
zT{1fmw$nCnGSMUNkwItvSfx7VE*PEQsJON<F?|9YP#T!U-O2^k(FoCJ+}F|L-R5Yi
zl-x$X<%!$i_YJDg6Zv;UpCm)cNteGngCo*wnUXrb95sK8M)jTdc<>|vGv3^qlL4L{
zggXkeDQOlg_i+$_J-SP|O6Cp}7(y+69p`HNU#81{3nhEM+`J@V?k&CPOTbyB8~aYc
z+Cu4tnXESojzB;2*<@?k5wiTbF-Reu(0%*n_DGab#=P7ove`-*o}G=w>G_7)3FRD_
zgo=16Wz{F>;mw$abBH93?r2HhofFaL!d02@xs-2E6Ka#m4w=9g=4&xg!nfn;M>>JZ
zghq`G_<6m&a?NF?VQ3Vgv<GW&=ytO?a8f`$C*bIkRR1iGI*Y%X(t4bVP&~96E^kL>
zH-ID!giy-2z&^z40xGZXbt?lMhlDx4+RSR+Tpq<7jARFvMG+&>QnIyCq+2JWvs$4f
zU79MXEFca~s=szKVRJ8ll)gXm!C)OY)tj9vs^mPWxRaMrng+tOny5yr&_thSQ)c6h
zAJgK;h47#ye=9ONvQ93Gs(zMCBGHIUChX#hqr<NE6+pAONiPSezdZt>C35r`!2i{V
zmca<jBGmcgVCH=SW!sCN4V-S31NmbWTrdudtO2V0l241-c!tuy;|*W2L8jTw7`U><
zK<~?qzlGB=Tmu=GUp*@?(1Gpjmg#m-Uhx3@Le{_#chp}%bc^V;e9W&-OIwHUWVc8m
zpL6L)zW|(c3oUtj=H;d?q|*bT3-3Zk@CuN>uth{J*>*^;{t^IhKg=?zyG2A`nBcV3
zwL;}rbAp_GmLCeQ;z3zubwO#xkcTdTWN2phPM6;#6OJ+d7F@mxZ@8=*2Cg)<BY;(9
z_X1CTx@bsJHf8(*v?!>L-VnNU&tHz^<Ut^qY%IT`)JP~O83P}L38D?1!0w_oY$ZVk
z1i8k^wOi;e`yL&7jN+#xu}-~H*}?h*CVL8n-r*wzXHN+M{i(+6sd7Zfzm{c!mFFX%
z;*Lh0GF=5@@f(hA*HoYEp7P68+7RvWdXlD_^>EwN2cO|!Pz`KLMW}zrOzKR4crTNE
zy%0${k2ZBN2CF`Tt%vO1=Gl+Ui^~0$jLdE#l`}n+rD)xW;xlM0&UWvWiZOq_VIXm6
p@5UGBpeoP7!>Zh?2A%Q?o<VJ0sZSg+>?_qUu5V<`GW>k({{xvZFhKwS

literal 15355
zcmb7LYjB-K8UA*^Bu&$V0>cb-28FaF1R13*2n@8P1+1q9!5;-=0K-Yn2^`3!IZ4`b
zsai1=u-wH`WC}R=%NsKlwNwziG6NMVpv)-cqJs*9KZL)c`#kS=_T6vKmo#)_-QD-P
z?`<#V%h+(WJUUbxt|r+(QybYhR-a6+tJX)W!^x&{J+T*-CzE+5u>)h1NqM+do=EIl
zU%xN0LNYK_8=kC<PE;q8bkt!kO|lsd`^%L|a^cuyd9pS(3IbzKBIO#}LdJmSDMqG-
zBZ^OwVr@nNc%H(kpBJ%WWn!GH<rxK*mq&Q()<*>cDz#UtLy2f}bv0?TWlScf%??P%
z+H=OnoXl1X7osuj9?tIZXxkx<98F%(s)i<jAJ(MB_f(4`s0Glvh9~iV$%58~Dy<Dw
zmRLLLypT}n5kTrf)0r2#B3nH`M<vSl>Y4ch^+;I?x<y=91zbNCaIIC;W}p@0e1csx
zIpwUqDRKXs=jKmm0DU|uZ%JB!*EKOUIM_dWgL3O}tF4X$=D1QhB6c#)mT}tVscWOx
zD!F%Hn=K`dR{<-ovm2Zi_n>8C;7lslwQgi1rfF|$j2Gsjw*Q7|eXOq10{TEz5R+AB
zjuuM|XuYO|OsM2yVXCafMd07<S-aFYlv-_|=tM)c)PA6yt6F5zq?XQ-f0tKlxY~~(
zY|boQ?tEyp=y>O(Ewzcs35*a)c2GKs7{oyzV3DZWXk}`UwWiH}fwUcg*wV6O2_~t!
zbz!mGDaEpcbgz|?C2)NTlumXTZ@r``VYaUk5NEi7F_YJ1p}VnOt>i)%LaFp|AY*k9
zqtk(BbJAyZusQ%1qv>l!yBdw@rK`?JTJ08$h25p-b+#h3(K`+e<%nOMDTm6#6V?9e
zaBU<j7;_LyV#hTzN-K<lf0q^r>IJ~|SvywGq(lp$gDkCgBycO?;xVxnjftqTNC$|r
zyIs+%x+UOW#i>ypUn>3HMzr+TMkniIoXo1vp%||RayJ_2KQT2hA*C^}V2KVm7dWO}
z(~brr<zi>zdUa?R7@6tEok|nek7UZy8(c!es-@BD(%4;Mq!avF#9w4NYk;f|j0x;9
z+L_#(|2AU^2~?8aRyvEi8ZK-$3qkQV&~u%=<jFe774@QRZMKfuhy<i%BMzm3gY2b3
zgm*TQ3h@~vRi!pDSg(!L+^GWF@;T5bnV(N*pJxmrXciQ=zBt3PoK#$Dx)@Z92=O^H
zYd#nFMS#R$m!Z3hvzMd$AZZ8Dt)Qu*DWSP83{p&d)lI<j_;=$8Xm3J8ZNH4(`r{cP
z%unG_<U$&l61r%-O`Zvd(-?YNUg8FB$MO}bv11Ku8SViAo4_p+s(^I1qU8b&1zg4n
z$q0ZRL(@6mUQ^!W%FLFH^;{}zIFO|@)=t)In`-4OX$lI>V=f;j>*dkL77(%Nm2ou7
zdd^tt6-%B3)nte3qMtN;_X5%tEG0|sh$X4WG7MkPK7pn)XISi;fnjIg&S^_-2Ft0%
zwcsZ)b{)G-#tzEQc3^a>uB$Ponw`}6XBY?WBrn>&$#OIrL9W7r>_jw4obE(B5ZVh^
z)FZY`FQsW%9sp(+>(Wc?=J%Bz%&}o6Jdff2!c`0blv{vWpahr(K(|05I2G#-c!TJ*
z7?om_)f<HG1FAqsuaWdOKwb|m6EhqE2B``o>F)rG-<0d?n0#|4t|9>_ELh6BP{12J
zR#oC1Rz%Py>Z~`x^mScw31b=~AM1l-Zhs4k@Br{~nUC=@Rg|GF3CBHJLR}V29m2ZO
z4&v1jF;^MJH;^Q_&|^lw8ZAfCTmoBE?3y+DRy#(<Qj+8lIKL^1s5-O<EtAC=uqe3{
zlL7)mn+527K(KoGARrx~mx1+fG;vnZTb=pk85q?pkYZN@mAI;uD@)~xiLt=~U$q_j
zSe^M#S5EyU9H_Ny=j={Fym(c@soAT_hl(HL$A*=MeER|mdbreZ-t~fzqH{Y@SVZiy
z$hzdWH?pod26}!-)}lSeU~T5j78+(TP?i*Gm(?UNDxvA~ii_KWG1DMiqeC}K1z)K;
z$OR1&+Q`CuKsMpi>*i#Se=0Z`9=2fvb8_A=<};W)B{WQ=K(K=BNYvmR$E7(9kT@=B
zPSwK5dLk{55k`&|a+=6(!QL2BIa%je-AW3fF=gysX_ggMJ32!0<tS?GQ>1ZQ4tDMy
zV6c%rv<+j1C?#52?gmU29*NAw0ChI&LCuvJIkI`21o`j-_lx6jQ(|V<9?(VQ%3K~e
zQ}LM$6t+j|#Zu79s-nY@xq^@x;zL<dIkNl|MXC?31OwXY@tmFKdP1TMt}r;{oJpqC
zipOP1`mbQN*$om)<g=Z0u~DczRg|XC(p15!+r)^%3Su{db!>lDKbXaAmW}7rz)GTH
zQAW$^bv@wGY2M(H?>GR2W0TpO4-bYX8w2P#nu)?i3^`E2v5B@R5r&3K)9uXMOh~}c
zjm_5rE4BoE<wZ8+Dhxq2JsTGwd;_wu7fQLiZ7%pyQ&=8%%!aSdq7>DSq<0jPI!(--
z&<D0NcNZg(Ggl5QF(C2p0mOU>lL8^V-}TMC0N*)VdX0dVR3l!0$tM|WrhN;TojuIL
z3G_wp61sBIRk?QoeESS?o7|}<ODduTI69e_yPFFg1c|g>DB_Qo=5|65wq`e)$S2V$
zSbThNCXK=15j5OBve@<ZB1nuTAT`<@QUT?4OCln2(Ko^N)<X$S-g9Vj?~0AGBU&RJ
z64%*VAm!$nq(m!Ge*{@dzsJkFEiyV%+1#Q*DY`^R+krH#S~LG?o9<i*AHxqq{@@S%
zrkxU*C5D&XovfNmv_mql5Vbjgxb`*x$&AZnGt*A_3LO~SdzCo6G3u-=4H5{KbfvJ^
zOMeB@Oiu;MkP47N91E|3fnJ|*;BZz99{vlh$ZbhX$p~Sp6kG9K3Yg7`5+^{L)r#*H
zTCo>&VR~`VYCtNPJ-KWJZnl|_nU<gb5W=-EVH@wM>T5M&p&j1`gS;K*b`3pKMbN6^
zOyqcWbJ)Qy*BM_!O+6x}lF>CZ+swfaXD4$bS!vmm1C^WxxY@gS$~~?J5diwSYiw)a
z3{2ikMWjxv2TBf<$QhWElpI|{xtW_=!1OS1dX}8kGYBo4i*R5)Bl28Vl3AXbwTgmY
zeDb#o-JCrPl;#7#86|ojb&t93>2F|aG7NwJP&VU@lq;js;f+*hA;r`gTG)0nuimZQ
zd)TFIat_Y>*659tXMAfw7T(qrpLxW4&XwLy;`|L%)Zf<ZiD0tF{b#N$f{@XkB@S-e
zfeD_;<HYnHV%C}~!rTECm?qKLo0GPqh<-yvZ_29qRbYkWFcn%!V|N1}{P{-oi(YH<
zk!vxu@^}~*WAHU6dy#gbblK9Cj1?;07h@4l#X@gDmgIJJdcg!E@GRHk0m`l<L-j@z
zJ~F~8{+dJKcX{1-*$+t1oja*emAsZ~XCw6jEi4q1t}7-5CXNhz7O)o-Bjs&RRKfo|
zAezDP3xd6n?8A5xC6yrr8vZ_dhJf5y0!+rfj@XL`LE!LANUdqwEc1L8*z+BZE%-$)
zkR6mqE?J5e!-wM%gz+eao>@y$)#U=lm=AvUv#OJLzUme@fb3Ma&jIti87$HQV0JG@
zm-~Te5$aAX*GRpUqOQ8F1FFFRC<}o|gU<qT&fGMh2}F%TJFLwwIg9j2ATwv-Oaf(L
z(1|~kVYQjSXvth{2+}3voM4ZRe6kXgYgEA?;UfiC0CUw03Nj|PI}G=`8`>84U#JDg
zw*Vq<5USP6NTF4rTmdGUF-f04HS3-i9GvI2=gDKGzJc&yketaCeH*ID8^})W-p?-W
zpfzuoU!a^Uu&vn#VkAsrW%i*W2<&aML*8w!pJckp)$>lwNZ67%Izw|e%{J)l?B~#}
z8eU@HEb6I-=E>YXtgOjfbB^1ySR;3$bOgLvT44xJ%1tx&<U<e`2<Y-o!y)}6Kb$k9
zsH2`Z?Xgs!E_(o7aoKmY`yjiFsaeh@_E;JRBINy1cFVw39xi8mJeQdbeo`LwqI0W#
z2C{JiF&p#*0!n*Y-qyt@5HhufLcH6|2GDoRcEGhy0_CYf<>k6YQ<fZ7_7u%^qu_*N
zWPa{==7#opYNPuAH%&PUJO}vxKxz>_kF1ucY+eLEO>FyI-Z1t6n7lAsk&)93SLAmd
z`?9F%h$Z%A?2TyuNJuYQ-H!IVk$q88?mmEIabl-PuNkT{4S6GIgG&Q%Me%+^VMqIn
zz^4N<eONaLeu?{dD*m)Wio|L_Po#++Mpshc5$%4LT`o3E0e-Ou5Q+~!l#m~aK5WNW
zR*jx~CG{w=JgWR4_+whdmqK||lV1gkAc)IkZ{F$&C;N~eqBse8R&L7&dG;(~-;XpA
zP2J}ovJkJL(aJ7AANI|+7c7f^MK$LI5#0g>sQ{VE6Q5sR1Jxr9xn3GSP-pyzq*2(7
zF_@+;<X^~iyGLp}1QH@Woi{U*Bn6j4$;5A;1s{?}z_cUpo^*kmH0QynJU@zcm}p`h
zzh4Nse9{x|7g;t?pJ~Uc@!o-M2~D(hqzhm<p2p-j*&Qk17ZqQT(>6z#&MQJMars`~
zv=xGf*f#46E_m`u52p`(<w)C9Gx2F8ip%MCk+wV+Y2?xZiA0!=#_Of(a5jYp(i4Eo
z%CWBT>DEJ-H_`V-)$!nC-r(F5XM@~)c^$5B%|CzuNx2_t_eYR%s(cK2Nzx7g%|^mL
zmt?#^Clvs~yQ-UqA*3<rah;3Z$9m;~iK%*}@asihVG>?z14>4h2y`DRRmb~BtNr2U
zN{+eQeGr>XKM(~MqAtLP+<#^P7okZPAu$%x)iDw%;evDxAwF~@CVPuRXW9|S1t1C?
zS#0!UZn}m-U^~e#>MW6!7g`XnjwtPLP4+Q|1}T`PLC%nA37FYuNEBc?8j<yV2MIr9
za~~7S=brv4I*2U49g$(OhC$m7=A4l2f-lJuT|Wg#y5a!Z?dO<XgU?IH@%=ZMoUNFr
zvkS9ifkA{8j2Rxx49H6_*Mh}_#eFEP$Zrs*06$YJd%z`>B*TCijJYD(h;04$eLn#(
zOgLv3emYuY7O}>na3PIPiGyW;<KeE!cGZ38ifw+OU2chsSO%^lKU%jB2+%Se$7EW?
z*iY(LiBGuc$eH|v)+?<nWx4dn)8J+#@v-i#_z*)rFMf%W{>0*Jfv@xR*9v9J+?8J^
zegz`FtEXGh6%cyCrzQI8?3hZXdu0m)k3}e*;-{yMRXU}z866UXzkwJr?r*jGJMI47
zb<-&>|5<ifbZ=6Gr`YX5%SO)PEf`Oup>^b*H4kGEF0~wP$Yx6Dxi{&}Qat&^uq@&B
zk05ayxKN_(9+b$*^-wOo3vjBH*}!gIjwxpX_k}XM>Aei9t%&+|fJlCjK_t0JLt=sH
zPQVY!82A*&B-s|=1M_}Cib!SAfIk5BSlxuFK*+?G)D%~?bXTiuliY5s3NV3XY2arG
z(VEAL9+~?5{WW+-`HR1WDhe(tl`Qg)<mBEC229u0)a(y#oJG_N+I<n-MMOBj*}$o8
zoDPx~?3eL^J;Ys<N~IAVAQo?-lMaZp!~&R^MnmlP(359?*l&!x>=`v8rT2uMt&loS
z>AnC{yB<G%au$3?&x=U<OX#cjsq|?#O7~&0vbCxD(F2B%Kh^3m^UlWvLX^*@DS!D-
z)Z<S>Q#mA3y{<@<s85i_8O!YYW>LCo<^-uq;J=m-mCEAmLu|i8iHdD`bh76DK%qFw
zqyo4wbAJ{?#_f)Q{Eh>W_P^BZ6--Ly`jdA5jIPAltFD*+C5|&UX+HpDZ&9ro2+%2|
zsk(u5hij5;)M^^tptdmgIOz_8&9&u?qU)7>cw%K=!2#AKIogA0!mE?Fzrs^}S(C{S
z-;t+pdm<@haCo{4c1$$1GbE2HtV%#4{y&MY0rIv3r0>u`xk7~LouGOTO?+W_yT?sR
zjpO=+f5iG<pxoBXT6Lp<nQPoTU_hqvG4dY{knUOnIQHpum)t<mT_yVw&UlR-3ccvD
zD&4JG>;@c;PIpq68Z$=1cAow(pZ6`GPIs#=yYps{Gr)AS8L-QAfLKa9__U-LN5*cE
z>%4!sk-DfSi}j6T?aSb0%taf^e1A^5Q2c|Tdxi{$?oU_)p!<`{V03j3=Kgpzgylw{
M`|N0CE&ky5|M0;Kt^fc4

diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index c6bc65842ccd20a45c5909da3004a12062ab89b3..52812acc8fec8f0bfa1ca24747441458ec72337f 100644
GIT binary patch
literal 15524
zcmbVT3zS_|c|QBxduK*rvNTOiO(K&pOfoKcG{LUO1lp2;G%f;3TwyIO(KwGYVRSN+
z%p)c>RZB&p*j9szQB-^s(AHw{(E{~Bu%R}fXwjNg!8FAP(r1b^YN7qV@7s@a&)h^b
zYh~x(d;j}?|NnlRn~AYvV0>hBtjPQyH#0uEvzVMJvi!=-IUBVmADo!Zb`DHt`Ra*@
zv8)}#HZeFeIyOBzp4Fx&XNoNLMh3=g`EW6k<(qbIFRnCvPlwCe(bhOUZe-i?fh-qY
zPB$9(M-Ar4E6+tVyJBK`V0v_795^mN@aOn9>&?;D#d2bjBr!rFZER0tzmX5(->d<`
z-GEM`WPm!GN$=T{)ok<(l74Q5@8<I~iFI?E*B#w^TWOA34vY^2F+06sT=Az7<&X@J
z27fxy%;B2RZQI92izy7WTGzCqBKgv#6rh`uKffaRd7Cu}x(lk3-&&fZ6veL5sp%=R
z=fxSR)ePJa%}YnhQEXoXq6-P00dP^!ZWnr4r@CyZX}fsrAbnsg3~IHvc}EdX5pgCl
zNS!3w37&<~&JMO{+F!nHJO0g<*k9+GHN1$yw1TQEQM8N~JBYrlVLIZ^!r-L#;3O|M
zCVK<*rPirZKl=8YOZ1m!(^qGCu`ODwK~d*|OuH;WkXoD#(4u1PxB_7Xrv`Rq`Otu+
z5{!;NZEgA5<%-+(JZI9`+}afyqOCfD2^-zcR@AVp9fT%}k+Bwrrse3!Xt|f#66dgH
zYG!Z>3F<8qNGI=vXaFl()e<X82-f`+k4*a5r{?_t`+_Z3TBq*p4_J=Oj2F9_c&;`9
zWEF~OF*0H!KBPdXt1aJ}wE?;WO@Crxg079YeUyTR>>@}hI)fCyWlN(J17l;eqyX(J
z+VcJ=4()B?Bo?Ij3Uh&^qsFV6dK&_}wMMOGIwMGEW<~AgrwGG_kAh1qPL@NO>{5dm
zD%l#9z?BTZ2Ha5xLSMs+GK}6TG|Idn#zq?nVvJ8rZy6n*o}7pp!kbu=JqOJkhU)JE
zR7PF}kW(>sUS%Uvs+b-yIx%uq0~huiA+Ww9NJg7=VNePEYJe&tuK{=kxo!ctei>s7
zo-#Lc{FMaJ(6N(%EOBN3{<DaWc=q#MLGR5rl1tF($<dvo17k#5$sFAcnB-T&Jp+SN
zGn2zjMv?guUNZk2tmxnpT3YrgFe<I6^&Cbfqd11$kfC^k?Xb!fLftGsh}GDsyt8{F
zH=0cPUrih`9!=ou0QPe9^#J>O(SnuKQYvzu1|*~+0Gue?R_mCRnv3X#dzk9OwC&c)
z_Hy*bYcvZw`(V96J1`7Q*lt!#qmU_+eJ$(&7WuABpv*Xdsm4+=IX4R)rJ(QSpv<$M
z6u^h)gDu6_XsP0c@Fnq1E@p(tJ=|P7P|33!(YzCl2m<N^)zNL+w@gnCjAIY<qL(~F
zi<VrpH@e6mp%)<4N7gd{#d>D~-;h8??Ox(C1ov8cdn(<)V(P{UGHoLvbs=W4<Cl_j
z6DWU_On)Ds1bkBh-<-g=0F;1#0B}<hkY?P6L1_%AS>8Q1667^me=*Ba%8yaXw}P~!
zyf%SvOW<_?A)0b?mKBqz%vH+El!{gC4~;+&6;%;`?VJ#N+UTG=c%&o`<@og!LGjcS
zu=intftA8Fl5H8V2eCo{`^NyK?w<fWDDjg7tUaAN?Y#pSl@k9)Hlhl%O^0ouw5Tuh
zWALg@Q9VWOySaqcr;8=d4H%uz(f0tH6QiN8hbcOQ(Tv50)j8IcciFJ7zC#nX;|y${
z&`I~Z;qaAC$VQZ8<{L1sq@Sa*04kn*KcMEF?R_@ld8mNTstqER3T!70kPJ(rDzi6%
zzO?>O0zV8;Uit{YW7=<a0M7b*&>luZ3p7jjK^vA+5C}|P3j`d{W>*<I6b|~!3aHIT
zBe6aTP-1;7fgcBWT(ZFVhW(uU>VcibmSWfT$;>4UkHMy5cueA&3Dl>|^8PI#(I=Zj
z?sAH=cvH1z{cbiaZ~d}@rK?$~jLN~sL0M;v+W<<hPbTnF0FRr<a$ILJ@Ch3%i7k0v
z?k@tj+A1%~WHB`{wzF8?+RV!{?*4PZM%n=SAp`s`07|0U6Zjbeo!#nur8$O~c*OX$
zbwU7+56?bXwGKa!=%gGA0MZR|_Gi(T2%k&f=K(4PzaWt3(ULVDN_I+tcxkZC9k!?>
zCHBvgM4_xhsgiXh+Fjr*(e6&*-x%l?s}$Uf;fxu@dKF9Uoi<$Ie~KV+iw)hY`z3&4
z`sD<E#Xz^127C&mo#KxmXvzPJHthLNOv*`3`YSf$ji+>pqcW=e2S8k++zU{nU)5+h
zza3-Y{s{(?A4DWL;~tw+RS2@c7BNudR1_=_@nMp}RleY6BU%0qSOUMs1s16~xoXb{
zY!BLGWLrH!Meai&;SW10QK*0_XQ*A&4i~@kx#9#`Rg(JwN}vZ4`1J&S!$2oJ9t3y^
zlkZzVIFWp6w;EZX6xs#vA)jzSExOTmmPUqEy*|zBQ5$B5(e!x~;$y#a>*%B-1g*)6
zP+8nMbXTEa&8s%SmWK=>93AY+JySmP!g0Y!D?q6Ojgt2}0A-qgG|0V17dntL6g2Xg
z_W74!z*Yu-Dj{Qc4sG=WaOj^{lfG>u^7Pd1Z8#`j44hW)E+NQzB_pupm+x@_{qitC
z#rh)vrOEdJ_V%J3LZfg1q<P*rbQz}+`zY-0X4F_8{>jFJJ;Oo#6hf0DUmX<an@kUy
zI@?4=3b2tP{|rzU&7%ON$iD!TppOC+?hgQNqSD6*CiN6Z7!)ei8zwVOQAhbF#K;jt
z=2OEJO^=yJuism`Ssmf~(Ri`t*?6i4{HZbhEp}<JRBx!m<3N|{KLRM#881@(Uv1Fg
z;JiE|m9v3WqSB3ir;-XD@<#$PCtCF1V>TE3XQzJC=NI&1g}?NpSCf7PB+yJ6r1dq^
z!2Expk<$MOP)h$7Kq-A3pq%*M2Dux#>`8#{Z{_cT^YV8O*1`d*6AEmMwWFXop4^i_
zvSbK{e>V(<11_9qpwdO|Sw?!~UQV`TBYLlZG_nyS+E3xRMam}sgL&D66<appb|stq
z6w5xvWj_P>XRT~f&VeYEY;v+}_^}a->K8lgrq%LFbc3OJM?DQtwelH&H?U~$1Go}R
zXR<lPWjb(%e%T)k|G$Q-YG}8Rt&=zwMuV>gq0)O5-Wc&`V<_N#p+aubZBRb#29B%@
z)(%|-og>WGESF<+JrQaEHxjG^<VNWz_9krs8%?ZTn97DpJ=u{g`y2Vym~{6`jshJ@
zaOqh9cXJU(VFz~)24i~upLL?~X@wOntuTO9neFpB4%qHK!ja7tE6~(^WJ!?m;JD2)
z%-nOaOjbAzAj8a^4p6vUwwVUuj<*S6=KdZC)I2EdO(LbKFLm5dRT}v2FqQ|UU59m=
zm2RoCG+f`x^Rhx=%4?fh!(;;!9}Q7d_W)ISKIUYBxd3H>Uje8%m<LdC@T&k72QL7~
zI^*U8Tti~N29S2ihG1&tS3j*z#xRE%XRic!f>sh5t<=uYGD9FJmGne>hUA!3sf2-=
zY_DY*f+lmoVjyddbcq_S`R;j!(T0b8C7C`Zh4j7{L~!!hKwwc@zM6pU<GQ^r;)saS
z!n2Z(2QnWLhU^w#h3vc#;367~bXYLli)=9GEz_L=@Ok2dgApPye+7YKJ^1HvV5h`G
zyt+dqcqXQYS$2+a6n&f(@vl3?7^GB;W|~sz;7gBtq2a}CkssOO1#z}vV)BuE)&=r8
z>6J96#L}E{N%Lh8NI8Z)%DT9xhk~L+Wgf1Q#_)f66G1oJ6&?A?mw46H7ZM3)UQ<rM
zefC^|KX_0Y#76)xKgKAqqL{mqoN^AP1fC0!k4o-5gYxqswj1ccFc<5km>>t&=tMjY
z1j`!ZJ`E^;nHCa6a{;jn%wci9%1{T(sMlc%-c>wvzaV;bJK><V6VPCp$S<JJpCFTA
z5GlaF^ybc0oPMW_tiZz_<T)x<pn)d|3J%80UxwxaG#8>N%Pzhc{p|`zic#X&4^-`N
z6h>iLQi1#`X5jjhn}O4@u)YKg6d<D`BR--rwzB2BUWgNjz!=HT=aJHZj(4|`AKl0W
zruSTMTsX-mt9FV;o33ow3U?8RD9C;jAWvpF%AW35CZn(BT(sZ1D=_KL6d`lr0I6tq
zbo;Q;^tr+309d=z=^0jgZ)uFKw#G|A)fz}vO2JJqA2GH-ai{m9rCFj49Lt@3-|~X?
z>v7{C7L>9U2ol}De%wO@lA$Q!0-cW}CR7?IPI!?C-`VolfdprmdWi+!IrD9p)(jDG
zlr{SdOifJ;#R^a^5<@`C8XeI{o^9-tnLVx<mb;9&1lJ|-a)Qx*`5W6XKs}BbVDAVr
zW&TEKnMhMmD$|+PJY;L~Yd|6zIKL*@hdIzE^lo6WY!->A5W;#oE-QMhFXIez2Hk5-
zE(J;-r(xRsT1*co^aB0pELkggLUIBppA1^=NwPve*I$uUYp698lz@@|-lGKh+YQ1t
zr~q^PaHt@Z&8jphw)|evYFn}lRhKCkM$|3ZgGE~kDwc=?n)&-7O}me!(b6Z_6gK78
zn1*4yS7A-cs{9u8p)mf<Z%IaCpri)2b`Z)9d*rOW2TNd_(t9vJ3tDLNdt>RTuqsjq
zmhouiUJbA$((Rh^BHdmQi3=&0L^5fV%;N9_7Dq3l(^}3BZ#K$VdQvUPDG^D5rejbx
zD9&{l#bACH8cEC@%Uz7AOl!IKy3HI3e!|aETH8f?CXiK;83GMay)f%8e>2PP1sY2<
zKhEa&p}#*iWoE6FgYi_l#cV73RpsutF|p#8|NM(U(n_hOxQyHeW~NKOj-U<r$SD@1
zSj`vW{2;*dyRC7wDk<3Sz)rbi=-GM!mQn_t+g^{p_N_63ORd$8u^7-{AFggOH_z-2
zASqz|{y?o1Gm0y18+Q_sp`_uEB!|i2VN7e5dGHAOMC727<49!?K?gNwCu>rRx+ycZ
zV|ghv7~C;gpCI4FqDe}>e^W|MXch#cv7hDkv*0YOqJSl9G!MGPOc5R!<%}6D61bCK
z^h=H>jr^%#&L1ap_F>}5q!#-6QkWkx$jw7viljwVA83&w=077PIHtTZ@O>(h@UyY+
z&kD_Q<WGWm$*ryUmXR0`(O|V&@I4B^tem8Em04udfY84OFuA|h<lvgNyCcBiL_Bh1
zWS09=aoJxMWL71jAPHG<_$E-S6o(ov-(DouC~i!uDeWo`yRk0CTkAa`sm_AI-?zB8
zU|~u1F7)k3QETyUtt&cKs;k=i+01VQDL`o+;RM}Vmwk#NMDerMy%k_p`4`(*O+tZB
z?S(+nN~!*43?$X7Ka!G+Np)^vQvGdMSW=x&C{gw0P+i~6s{z3GAO&bDMjAY|X@mpQ
z;A1p?jvFqe=}4-FBpmAe=fk;>gDY1sSl@xZ^8I>(NT=+^xN9W>`C+<-1gQ6%fU0;Y
z{eGnO0-<(;7MLr%xN1MTZ2Ugh$Y-yAadka?R9z2BJh*uM!y}9ifyoGVV+U&OqNKnv
z4Cuk+T>xc)cPDV4fwhaM;l8K_>qPBJ<qZ#&<^3nzrSL57Z*mZ<{LAh5o{-GyZ&Zw_
zl3(7FM0qd4VC-G!*%c!RHA1yW;OF=yzc-@Reg|Z#77a{hc_hCpt-QR|N{mHc*g>-T
z+^wqt-cf*Adu=3_m0a-w%*hoWOyErh)?Qn21us^$opJ?V(ObC!aaMALUEf>f2w0uN
z2=i%YefMFEN|uih47O=@0GH`pLy#8b+X|AX*^Wd|kp?Iia4qCKWm0e{8@>S4=!5D~
z5Q#p(Q^l#B;B}_`btwA;C`ji&P2ep6&#Bly+hl{a{j&dufYHkSAGhJM{r%7XThu8K
zIG%!nwO<wLHcUyVPZDhHh(MD@;iHhwKJ1^QRE0J4N$K|~>_6+=$Zkq<(?!*lkUIHA
zHu!nIDcPbQ>s6~h15md3%LLv5@Oafhdu_0Gw;XgUFj_eXSD=!E_^qTxiukn6^xgaz
zh)JN&0hB<WPv92-@?*JsI*#(uUQdzOc}mi7hlmehpS3wJl6^Du&+FkiOxLt}>3w}8
zXk|S?!mGGN`*-B9i}e9z6};4HVgonAzXnd7;GF>V(tH=d9**7(@Ty*G+|zA<d5$1y
z8i4xMzKa>)*S>+~n<&$s=`sVeH=yBX5ZOcPZOr3iI-26IFz&xIU@IA!n6%&Un}4ci
zNV`F{KB;NHq)@S9HtDGUWiXJMUjev?3S9?~QXkd665i5F|4U@Cq0}DbCCkA__KgQ4
zkL!N6mLn`9Qj9#iKr{7gk41?Pt@?mWwvPd?i@aeseGSN1J~{trIOfO%A$zKJ2;0li
zWCVNmkrDc(8K}$Se+y8iI0#T4zt5oBQHYnNjXy(_)qbjE`V!_!;TzrcRU0lPQ|Z4M
zVL=L7@2w;wY*qU=AT5Em`YtHR4q>$7q<ULY<xI>k0jXpyKTkt035IL+ohpgs4Oh4S
zi{q_j1ZyWK%>y7VX}%6nb^`T!TiH%YpMIc$PF)|O+}AMB%4B@1X!?*gGd?mgHr({p
zI(|#j!4AL60=fD;sy)|0cOWs3|2srK!CBA)+~sHrH0@|8;3{hOE%X->{0D&2?jeBM
z6u)gyeIEal20w7=MVRSYUko(6*)yy8<VQx?DrVI{52nvXGmM5Qk-kpVmnQjtkmMhx
zEZ^ZOA|wq;Kf@?&-W@_5@F}Lg)b0xUPha(=V4H7ajF4{uX|f^Ut^-8v3$S5ox^*PO
zDO!hewnvHFI-f#rT~(fEK!a<*sD7RaF<$7$H8cd-OKl2;yJr12(45P%!H;i}s{T?N
z&iWBh`NKdi{qRHr+mQPSCM0AyZhzB8!hWG|jtZfsPyVe!h{_;(%HJMSxv1z``VK&a
zK(Y29jOh4UqY&Z^P9gMtP*w;XF{pl-V!}Xo0DWv9wFj+9FZ1pI)URKF!Q>zR%fAAn
zDSGjqv;sr*u4QOxGW%Go^wkS~iW~(XS7XPi^9Kdmmq53^(V7&<_~y%yu3s4iV(8R=
z9eBFIK0=Ogv!aSt(T^09+hc9~p5e9fQryhS-^_iUlL6DGVXN!&&|C)4J!Xwh+Q$LP
z;y(h&vo{|S!-7yP6mbZbQVRQbDN`83^~;0=X=fvai2I?<Ik$eh{SRMX<JGY(Ium4f
WJ^{Fu3mWxjUw7&F@EZKj<o^eCcv%4e

literal 15446
zcmbVT3zVHzb^gzP@0}UINilt-O{R{?WWrRWGyzu1L>plw3|*BZuCc2^Xfl)ehs^5a
zPBM=WYGf6Y*0g98F^bP3Ds&0fS1UfDCe}d3N|mftqEH;c)YUcx8nw`e-QV|}$A9nK
z1Z>vg%>MV;XTQ%rugl~_F<c)TpC~f_&&}4ycNJ69MV7xVbI!2V<Rg<a*{<QKEWdPe
zaw2O7+B!yN$0ugS>se)HYPQJY*Vyoc4IeGWvV7?J9mVU6-t*zGcC;0C*NtskKAh#^
z%kEkYf7GClvhrL^vnwZOhG)hn>!5M@p}X-n>&wwrC313#EP)}DHnwN+yOxjOZ&m~2
z9zbVNGeDh<toQ86Du#UtS)bV?chmXm#JGix<L37NMX8Tg4%bIPn7ycGQt_`A^^gwG
z2LC$IEZ~^&?K>vMi)kQQjcXXur1^>!RG^2Nzqm>B^Easzd>1!serKtVS`@p-r)Q?k
zpO<9hRxxlxbT0#`K(YN*FkM3MB>=mEb-VGEb?TEXEp3;Ko#YRSCBdxrHXkU`DI=DV
zg51fXo#1j{J3H8-X}@Co4*boQ+JDY9TKGyP(<+*>RM}E5c9Q&@n%RhdOG1#^Ly)}Q
z=<EyJSJ+20_qjj4t;BytHnT0ui|x@{HLAK0Y}(}sg0$l004*y9>q>-G>>A#k<y(hs
zD#7Xa*VdK~u2kN(=Q$^x^$o5PioWUyF0A!98&Scqb}*VM#wJ=gnx11IqvtNPA<kjU
z^z6tqCaCvJV4b29vH_y#Rhw8*Lx>)rdKA*nZ(2S8us`^6wS82b{e#G{*?O_NLFT2V
zfV@IAEl0)-<5LQZy4&(=vo=7lMl+B^n4*J`wx3$ik=+ETMQ6}rtqqM@3{OnV(*nG&
zY|96tI`p@xlSGi?Yb^xQjux+J_}UP}4H~zK*^DHio0YY%IZYbYd=|Xg@?<5n$u2X9
zsgkWz30%zttRWm#5cJo)Dx>&XgGMtisIk#7L5*T&*ldfjz7*83c#OdMj=+mnb_1y?
zcojfR`>O$7$&}s%aQ!*V3i#FnL;UX%M8i<9klR#~#|D;@9vSHSyMv~$H%u;n%}kB&
z8Xuk@(Q3}BS-@n!8V(&EnVy{*je$~9f&>X6hb_Qo2Zu1ZRAWX+MC?|83wnq^6BA{N
zeMpaDr`4K}oF;^$v9|c|^hIfOnd~pXOw#CBf!6}tN5R_w4)md=4n%755TpYMY1)D?
zDu+0mmm167EB0`5j?%ZIO$)-@yWgZ<@HqhQjo1>ub<)<KVg{v0bI(^VP8`Zzoj|#f
z@u;n!kYCS2M5*Y_L~e$J>>!$U$l;2<xtJI))kw@H{3G*D4xYrfyu>-uf!dqhf@VJ&
zF$B~JuH)NxY@V4Ku4C2ms+S@|kCsBTFNVk<kr!aqPtj8VC7LU-z?p<)-t8mpE@1cB
zg!EjPIh<^9&SRwslMQMXJO5vr4nfifDD)2jN~<>{a8Cl?2v7>%0B|TNNH-n;QWgVh
z)c1PB1bt1{pUtz>@`Kd!MzEHaZ%W|a1nvU})igKfc`>QVI!1j5Fea{9e`Fs))%xVj
zX8dO>dx&YRgW=#NkTO)cm_Ie;Q$xZY26HA>O4rD?Wx^i92qo-I0A=o503MS1NdwlN
zPVLX$42q_r{AY$yh1ss{F-Tg}mqjsoRi|j4GM90c4sYXV2IB1i7ZJP};DVS9{k@!`
zTY$}2Y*?LRU3sgaef8ZsS-1JMV^Vw5hr@O$?P-lE*(@@kK0<JT$^y7}_6#4>EyfU2
z+RIP@pH~~iEEU*JIv_cgOjTyz14(kgdlUFRfQr)l0nTZ?sRPaideI(5Lk~1+cdMZl
z6eI$tuO$MuRP(EhZR1A#@dDfyp^;i21SqxsJb||XJRw~We4{=i-!{Cf*j()1F_pPw
z;T(J_fpb#VT%d32tmuCjEc)eh=v|)TEZ#J&(Y_BDmG^$xz|vu=R7Mrx6X3jn>GV;6
zvg?in-U;x8sjR?tCI_E1WJzu5bA{i!f5b+4Ri=vR$%$RX%GPdPnJtHeg=l0Apzl+o
zy8ud~yA$|v1D)+;e5IK~PuyaB%sxT_)<-vwTb@szN-zd0{RmNy#Q+%w1^biumI|Lr
z;HLp92R|c_JIInZ9!h>niFjG?&L?b8NlUDsr^rHihgv1?NVR()S*m?5fuA?fb*U5}
zA1n{iuwKP!`dPy?$v;h!xGr#zxnBe*p<hbimko4Xbl@|<c1k{ypr!mT7~0F9oKlb)
z>{o8aGfL^$MPpR??*ntG@;3m5{R%)F!&U;w=2*CY1Te)xOhPd3wLVpapbLBv>y(0u
zf(0g7XH&W=7GFh|botu^ehpw})P*sK<@m7mMX}90s3?6aSoqCOl1u}Xx}kQ_Ivmw5
z;E0oGRY@KIDBb=pfnQJHg9f^_oN?a(_$q?m1i?wlWK8WGA`g^OyEp?xA984m9<-e$
z%&4l@$9SM=L+>b>eosPrtaomZLHaI1P!uMLZg-Tp1~}Hd<|c&jej^B52RkIsmN&f!
zTyWAVaOyy#Z2mStx#nSm+*LY)ft`_{QOvZ?p9@4Oo|=#;y!6#^&@eu+CVk5=iuCmL
z+p$r;1T?K~N<xzLNk>pAzaHTL#^o45<@$F3$`Uv)>+3_i6^+sXkotMz(D9j0?5DD`
zjij+Y{G;K6Kf^}+G)hw<?+G;NhRhDSIvb)P1;ogZ#{lY}`A-04$m0N|==T7MmX&>o
zMt>jJp=6#CDUs5=Q3_)hZB%?hjy!7Ayd1c);remzrv0Up)uX)esTZ4HNThlppB6LT
z5|@yrdP5t20CJhmB$4U=46IE5p+OEC=am_`yc}I6E<O0})TBa${FZ>iNfzVxr1gdP
z*{<L0`5B|wBwzM1s_dcB1vF4kLel%{siFU0(a7k311O`p>yXj^4y@w+ltJzm4tpBl
zJ6pxOV87zsi?Pr}bwY^^TssPiy9r=YNS+Mo@GsWKbijer98@~Uy}(S5(#w-A`H0ag
zpn`m4fICR#{{u+*gk@Sj;Tk2M{1^oC$xjS&cW~H$0=%=8Pej_%C#RYXDCyDsVyB(7
zY!4FaWL)id@Q_l^*$7`N{|n&TShNoS#O<FYrZw_8)#Y?x594w$IR06X@y^UnA=ge}
zTNoXFDHxURt8gobe;Y#q?++DnNT)%?v<EcuGDZInzUAQm1*qGsp8{MD0tYDDNRTiW
zN|ysWq$OaZskIy5*(kXuKT_mCE#HPtcfa%~@IehOTMlrRgNTJ695zVlr2F6Y5uHyj
ztZM0nVT{5SRoeku-N%U8)Z_)ax}PEmG9O$UXz2yV2+#|z16W4XaUB-znZRzML$D&N
z)Vi+$q~*bA?-ChJduii_W}`vxcnk|Q$$@#J(JgJ3h3i{IUS257c-Eh69VZ)f^w|(q
zbq~-KF5dFM&w)%HI2)ky;Kcxy2MYlz4}KmX>x}yafa}QY7XkVu2(DJm8KBoG819hZ
z3{%maq?bfSFSRqZ%n`^rO?nbOM|RH{Qo9^E8=vH>VHuJpbD(kr*+;$*9Ip=@GN27t
z@tS0M{t46j5|Co&!K;C+t1Z`*!-Th!7-v8iX~dKso;UfpA(NJL%_1@-_{#vh2>uE{
zZm!&7gYq+pT>|h$l7x*B3SItM0&~6ib2Nz4#6vo|BOKa|?$H%!zia=wBY?11#9w!0
zIsQ;9P6Fn<rh_j%?w5=pE{l8?iwDH{j){|x?6YpL&pBmEmM?=$Wf+3!EvF`$V>GFo
zYkDXsny8#+Yh*EpiYu5<>2OwbOAX`CO1Rb4n}(FLsA*0he0E)df4EQ@!6SgzA2_mB
z7XKQ)6_l4H@LYhrRB~9h^7H$wb=R;~aIkKQ2@<(ZJK{gUIJ{5{4$lC}FVsMSXf7gk
zfj$h*R~zX_nRG9@5MAXu*9($2FDFE5IROuriTomZ`Z$G*f=L1Sr8{?yV)uSIS&4@=
z$V*hNzyi+_9Nab5<QJm32+ePzDeEq|z`mkMBGo8K8~|zlN^3GIqqHoUKzU7W;P_L!
zf!(pNf`Lzv@v$+V(ZF5M@?J0G2~=Q?<mYos>A=V5$^amFCd?f=!<Q7>F3h`F8N`sR
zovLx<>Y9B!ri}89Rf9XTd<e9jDpYfR9yG01q0{dvg7k|GBjI*Nw}*{}t%{!m5bZh`
z85VQzX<*k{<Fo!%1W`n&1=quT#KZ#cI{MHe`lVf4%sMSQ1G?Ne3?fY}y2~EGyz2h;
z1NRD^4OIyT=zJszq0tyF6~RM7c+aNgp4{ojB!c&x`8Wiq2haevvgV)R>FLR>u>zEf
z#8!}Hwd5o(HaU&D@G(dWmqK?1hcTePO)&Z|zpf1k+A(K<-6P1A`E{}~v8JLlrZbIs
z$j0P1fJL-DzajaDbD&@3J)mOQED}=@gz>6*MX!C!Iiu{s=Z&V95~ZKrV??5RG?9~A
z43@l=A|X9Nlh=clyOXZ4&#i6JRbyy143vV>0MW~DMDxeiU>Q{G-P%T;cCbc&`UwLE
z`M5V(HJ&^})8z`-s_GN{!J;h#l}n_73Hdug&DTBLhn1dSQ`(eoV`@h2eivi-3d32I
z-;Qq>jKBHq$si_5YT#?Pg^ef9+IumCsZBafW1rf5Z!BFEHmlTOW3{z%R{<=kbeFok
zN_RD>#DP(s+hW?N4oSjs431I6M{7Mh%6gWrR7-kFMRK6)HUq3toxKFD$$3F5jk#jE
z-$GZWv0QuI>xl_*!VgJW`$g3Y#Hz?l!J4>Uob{C7%<}s{#uClP+59lR55}e}thI3r
z79~m;^R3yq`;DPQ@#R1NJOpT@OxprPOu?Dq*_qNEK7GJTPKjXR@`gA+gkcx-SmS;l
zAoaChZk=|;(6#kq(xcJ7Z5u!pKc-?zB;JPSM}4}wF5Sm`0`w|_etq}?G0Yj|m6i=e
z)~AxtVUiqOVfg%!)XRBr4BsRqCru9Qe#=NC9n73RS(91xFAp7VJBBBNawd12tj8%g
ziD=ML$ssM-p<XbI&VGT*&tjG;Dp+z-Bhu+4v6BjOwoD~(njpP~{Y3sWnrDJLpHA-V
zN5@miEPU&wFy}df2SOQ=21%zB0}TSFpG2f9jSO<1i7b3?{Puf=Mm_SUpiC*Ot>l)8
zj)6WpEdObUJqp0QIk}k3(fB=#LGC(yr|?(Kz;_6L<&2~sUE&9-Y|ab6dcojeS&?~_
zh>9d)<>4DJuBkXwuyyk)sYYE3DzCrF!!BZCzO`NxlIbiM+S0rcBTJ^^FlxUbl5v$K
zF|e9k92gvv`Gp`QDBUBPU^`W59R(3ep0y4O|2*TNKt)PHPK9?48Y$EFU{q<UHT_6R
zIwsS(gvs>17+5m>JbXvf&x2&Wn`^(5=07h{l%U5zM6-qTjyr{GL<860F&aOh4TsXS
zCDla|Hg*2_5aHLO%c>f%Z^pOk@P2}rPT4JS)k+NVqYMoh(C!6+^m+`jU2hNmKvrd;
zNFze&#Zjfz?$qOZo5wRo&Ep}Czi0CHhf5f30+SQ$#17KR#mRs<Aowir-U?72IFLYG
z%vLU@h6kb<tP_=unm2y};#4W(?W22(q5XLgij{wB9q$v8ul$LMImL)7E;oa@w0Z}@
z;H=&FDmyzLp;=_`JaNhIi=>qSuxa*a5Hc^K`DfF}D_V^NF2=(4wawSvBOu^AEB;nC
zMRr*!6z?Vt^YYdNzJ~*vLcxPoWlEuVJBV9_;$4O=g~E>St>y>@pT`XI)6Tx#`+!vd
z-cK<2rZE5<#<gERu%<_Ow}MI3=tt73NCQ*|IQDrb1&2x&hcX7uL!oAj0j?@e9|UhR
z{jW{ghiEAMe|rKy4Dh@r|7X||R1V7j?*&CG|KDclvj6=L_FL2`FgTHtf<;g>;iKqM
zAnqX8IuL;;ox)3@j8lT&rzlln3}d1n9&il5U+~<>ZcTbKM9m|ib&898@O-f;`GPZ5
zwd&(^00Z=w3FO}RM00@l8A0V91?VFnZWW-r4P6Ql-%46c5nn+wy_=V2?5Dt2!TEFo
zKLe1D<?h*t<)yu@B4I#D8!Q>Ae16hCyh`?F=&#qqb=V~!&8nsQ^^L^z1`V&~67BDi
z!z$Jfnl*@0tBwuy=U;=SN{~kg?TqgMwwKt?0ld1;8ux4)U|yG#H61|vDi5Ov^p&rp
z`3BYwFZ3J(Gj6K+3?hGMJV-?knt1d0SHSys1}r6GlT-Gqdy7xA8`5%;txsm!FJn}!
zIGbKdE4~B)GV{v-yJ*l}fYkaiD4d-Y?$XnxNcK|0S03jf%OOVg#skcgI-d;^!!jbn
zD6<<p(|6^Gs1dR?J!V#(09`j_!w-55$Yudjt;fSQM=l7nr`Zo-rGG3r!LEJegaKIw
zmWucxfO5rQfQtB64XQlWJeiPXl^<&|eG$Z^^o`;AilIxBsq{YvVL(b+AFZS#d{y}&
zh?X))M*vE*`vEoushTHKmZ5(sSS4@yemZh#a9pc*s-%*4Ts04YA25cMlhlSkYLYf&
zDL*}E1l7Fkr(_QXXEPwsLzEsmTe<83BMOsU4@R@~vB`<ihF9wiV28J~VFLJF7J%y6
zG<%_e?%pIk{{I~M3C`kP(5^&NpwapOXbr9VCcq^G9|9=r{sEvC#cvr@J)8fN1|PU|
zBh2Yq?E;ydV6MYoUinc_wuZCn8j8k)j~-t*CDQ9uby?E?drALM>hf)lB0;i1SH`rU
zuzq(0dBCff>M}bk=zr6yE`!*7oH;TIHtEqu3>cmQVmLM3AlcBT<V`)>qegDfPa!wh
ztj}}c!7&h2J=c_|7y5Ax9YOIjn@Wv=3O&`A=}ly*!FuVf{szDSBvk$gh)X{_k-~;@
zKSGC;3{Mw-Z<tmov?|ug@^fq{g=h@2r~LMq%0-i{rFQ@tgruxI2q(H@;Gq=y4nU=l
zPIx4E)R5K7l@kU!yj)aq46R@m@os?ba`(dg>P0}N`1oJ`6~NMTx&!CtRX|mjoP(C0
zw8vT%JKf-?%uxbzG*+DI@4z~(OW<35jWsEe@#f2vu5OG9F?Fg;W}RS<^<oV4R#wp~
z`jKJ^d#sI*7+tF<oi0ceK#4UQT|FDk<pAB2)_9Nq0H8d693c1Jyd)0;LbXuFAzeyS
zSjX*f2~oXVM9_9VQOLL_tk1diJM90-^)+4}wnS%w?93+sr*c8#e(&optB<b3|4aOT
Djz&w$

diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index 27be7341f..4ad3a76e6 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -22,6 +22,7 @@ MK_CONSTANT(subst_fn, name("subst"));
 MK_CONSTANT(funext_fn, name("funext"));
 MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(substp_fn, name("substp"));
+MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(eta_fn, name("eta"));
 MK_CONSTANT(trivial, name("trivial"));
 MK_CONSTANT(absurd_fn, name("absurd"));
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index aea60526a..6d9b63d71 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -58,6 +58,9 @@ inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr
 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}); }
+expr mk_not_intro_fn();
+bool is_not_intro_fn(expr const & e);
+inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); }
 expr mk_eta_fn();
 bool is_eta_fn(expr const & e);
 inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); }
diff --git a/src/library/arith/Nat_decls.cpp b/src/library/arith/Nat_decls.cpp
index 4eff54b54..bce59a39f 100644
--- a/src/library/arith/Nat_decls.cpp
+++ b/src/library/arith/Nat_decls.cpp
@@ -19,6 +19,7 @@ MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"}));
 MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"}));
 MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"}));
 MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"}));
+MK_CONSTANT(Nat_induction_on_fn, name({"Nat", "induction_on"}));
 MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"}));
 MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"}));
 MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"}));
@@ -33,7 +34,8 @@ MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"}));
 MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"}));
 MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"}));
 MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"}));
-MK_CONSTANT(Nat_add_inj_fn, name({"Nat", "add_inj"}));
+MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"}));
+MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"}));
 MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"}));
 MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"}));
 MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"}));
@@ -42,4 +44,15 @@ MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"}));
 MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"}));
 MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"}));
 MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"}));
+MK_CONSTANT(Nat_not_lt_0_fn, name({"Nat", "not_lt_0"}));
+MK_CONSTANT(Nat_lt_intro_fn, name({"Nat", "lt_intro"}));
+MK_CONSTANT(Nat_lt_elim_fn, name({"Nat", "lt_elim"}));
+MK_CONSTANT(Nat_lt_le_fn, name({"Nat", "lt_le"}));
+MK_CONSTANT(Nat_lt_ne_fn, name({"Nat", "lt_ne"}));
+MK_CONSTANT(Nat_lt_nrefl_fn, name({"Nat", "lt_nrefl"}));
+MK_CONSTANT(Nat_lt_trans_fn, name({"Nat", "lt_trans"}));
+MK_CONSTANT(Nat_lt_le_trans_fn, name({"Nat", "lt_le_trans"}));
+MK_CONSTANT(Nat_le_lt_trans_fn, name({"Nat", "le_lt_trans"}));
+MK_CONSTANT(Nat_ne_lt_succ_fn, name({"Nat", "ne_lt_succ"}));
+MK_CONSTANT(Nat_strong_induction_fn, name({"Nat", "strong_induction"}));
 }
diff --git a/src/library/arith/Nat_decls.h b/src/library/arith/Nat_decls.h
index fa0830b87..d7ed8f6d9 100644
--- a/src/library/arith/Nat_decls.h
+++ b/src/library/arith/Nat_decls.h
@@ -47,6 +47,9 @@ inline expr mk_Nat_le_def_th(expr const & e1, expr const & e2) { return mk_app({
 expr mk_Nat_induction_fn();
 bool is_Nat_induction_fn(expr const & e);
 inline expr mk_Nat_induction_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_induction_on_fn();
+bool is_Nat_induction_on_fn(expr const & e);
+inline expr mk_Nat_induction_on_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_on_fn(), e1, e2, e3, e4}); }
 expr mk_Nat_pred_nz_fn();
 bool is_Nat_pred_nz_fn(expr const & e);
 inline expr mk_Nat_pred_nz_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_pred_nz_fn(), e1, e2}); }
@@ -89,9 +92,12 @@ inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const &
 expr mk_Nat_mul_assoc_fn();
 bool is_Nat_mul_assoc_fn(expr const & e);
 inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); }
-expr mk_Nat_add_inj_fn();
-bool is_Nat_add_inj_fn(expr const & e);
-inline expr mk_Nat_add_inj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_inj_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_add_injr_fn();
+bool is_Nat_add_injr_fn(expr const & e);
+inline expr mk_Nat_add_injr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injr_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_add_injl_fn();
+bool is_Nat_add_injl_fn(expr const & e);
+inline expr mk_Nat_add_injl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injl_fn(), e1, e2, e3, e4}); }
 expr mk_Nat_add_eqz_fn();
 bool is_Nat_add_eqz_fn(expr const & e);
 inline expr mk_Nat_add_eqz_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_eqz_fn(), e1, e2, e3}); }
@@ -116,4 +122,37 @@ inline expr mk_Nat_le_add_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_Nat_le_antisym_fn();
 bool is_Nat_le_antisym_fn(expr const & e);
 inline expr mk_Nat_le_antisym_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_antisym_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_not_lt_0_fn();
+bool is_Nat_not_lt_0_fn(expr const & e);
+inline expr mk_Nat_not_lt_0_th(expr const & e1) { return mk_app({mk_Nat_not_lt_0_fn(), e1}); }
+expr mk_Nat_lt_intro_fn();
+bool is_Nat_lt_intro_fn(expr const & e);
+inline expr mk_Nat_lt_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_lt_intro_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_lt_elim_fn();
+bool is_Nat_lt_elim_fn(expr const & e);
+inline expr mk_Nat_lt_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_elim_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_le_fn();
+bool is_Nat_lt_le_fn(expr const & e);
+inline expr mk_Nat_lt_le_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_le_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_ne_fn();
+bool is_Nat_lt_ne_fn(expr const & e);
+inline expr mk_Nat_lt_ne_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_ne_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_nrefl_fn();
+bool is_Nat_lt_nrefl_fn(expr const & e);
+inline expr mk_Nat_lt_nrefl_th(expr const & e1) { return mk_app({mk_Nat_lt_nrefl_fn(), e1}); }
+expr mk_Nat_lt_trans_fn();
+bool is_Nat_lt_trans_fn(expr const & e);
+inline expr mk_Nat_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_lt_le_trans_fn();
+bool is_Nat_lt_le_trans_fn(expr const & e);
+inline expr mk_Nat_lt_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_le_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_le_lt_trans_fn();
+bool is_Nat_le_lt_trans_fn(expr const & e);
+inline expr mk_Nat_le_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_lt_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_ne_lt_succ_fn();
+bool is_Nat_ne_lt_succ_fn(expr const & e);
+inline expr mk_Nat_ne_lt_succ_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_ne_lt_succ_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_strong_induction_fn();
+bool is_Nat_strong_induction_fn(expr const & e);
+inline expr mk_Nat_strong_induction_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_strong_induction_fn(), e1, e2, e3}); }
 }