From 2bb33c55fefbab83544fba9be4040ac80e2be1d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Jan 2014 18:52:50 -0800
Subject: [PATCH] feat(builtin/kernel): add more theorems useful for
 simplification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean      |  36 +++++++++++++++++++++++++++++++++++
 src/builtin/obj/kernel.olean | Bin 27339 -> 28944 bytes
 src/kernel/kernel_decls.cpp  |   5 +++++
 src/kernel/kernel_decls.h    |  15 +++++++++++++++
 4 files changed, 56 insertions(+)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 3e9dc4f37..2b92e86c9 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -210,6 +210,10 @@ 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 nonempty_elim {A : TypeU} (H1 : nonempty A) {B : Bool} (H2 : A → B) : B
+:= obtain (w : A) (Hw : true), from H1,
+     H2 w
+
 theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonempty A
 := obtain (w : A) (Hw : P w), from H,
       exists_intro w trivial
@@ -333,6 +337,16 @@ theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a
 theorem imp_falsel (a : Bool) : (false → a) ↔ true
 := case (λ x, (false → x) ↔ true) trivial trivial a
 
+theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
+:= iff_intro
+     (assume H : a → b,
+        (or_elim (em a)
+           (λ Ha  : a,   or_intror (¬ a) (H Ha))
+           (λ Hna : ¬ a, or_introl Hna b)))
+     (assume H : ¬ a ∨ b,
+        assume Ha : a,
+          resolve1 H ((symm (not_not_eq a)) ◂ Ha))
+
 theorem not_true : ¬ true ↔ false
 := trivial
 
@@ -384,6 +398,21 @@ theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
 theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b
 := congr2 not H
 
+theorem exists_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∃ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∃ x : A, p),
+       obtain (w : A) (Hw : p), from Hl,
+         Hw)
+    (assume Hr : p,
+       nonempty_elim H (λ w, exists_intro w Hr))
+
+theorem forall_rem {A : TypeU} (H : nonempty A) (p : Bool) : (∀ x : A, p) ↔ p
+:= iff_intro
+    (assume Hl : (∀ x : A, p),
+       nonempty_elim H (λ w, Hl w))
+    (assume Hr : p,
+       take x, Hr)
+
 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)
 
@@ -573,6 +602,13 @@ theorem exists_or_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x ∨
                 obtain (w : A) (Hw : ψ w), from H2,
                     exists_intro w (or_intror (φ w) Hw)))
 
+
+theorem exists_imp_distribute {A : TypeU} (φ ψ : A → Bool) : (∃ x, φ x → ψ x) ↔ ((∀ x, φ x) → (∃ x, ψ x))
+:= calc (∃ x, φ x → ψ x) = (∃ x, ¬ φ x ∨ ψ x)           : eq_exists_intro (λ x, imp_or (φ x) (ψ x))
+                     ...   = (∃ x, ¬ φ x) ∨ (∃ x, ψ x)   : exists_or_distribute _ _
+                     ...   = ¬ (∀ x, φ x) ∨ (∃ x, ψ x)   : { symm (not_forall A φ) }
+                     ...   = (∀ x, φ x) → (∃ x, ψ x)     : symm (imp_or _ _)
+
 set_opaque exists  true
 set_opaque not     true
 set_opaque or      true
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 5189b515f8726194f8f47399c3ece73042c34b65..a8fbfea5d8dce00f3c96465c3aa63ee4c0231db9 100644
GIT binary patch
delta 9507
zcmb_hd6-qzk-z8Ocke}L5Tu)Kdf_$n-t<l{EDdebi!@7`ErM*#(hao3VgPqzw<eCx
zr!%4ji6|MDQS=)Ph~pB+jLv+<Oq|S&OVpVNYS0+KCBacNah>{A-TUtAr<uQo@9W}s
z>QvRKQ&nfX@0Tx|-EW!)D<@6e(!bU6>{bi^ay)xZt)N|=JzIdwtU4B0C#^VWnh@GP
zDI;^2%h)Ui!xgxMk=;wXC#BEs0>i2X=>l;;L^tl*7o%Zyx%M1I=ro^nZM^_&)6K*&
z7EPFRZsmF4<cRSVfaL;LGO~A;fcAqM7w#&$f6^ASoU#h)dUqCppH>8V2}rz123Zbl
zMHBJSOcV9BfI5^+SBF~9%ppUe4U6`*^!%hO`gy@w=KJ*Pf@0HibK&1NZRDQ7$R@zm
zVtO+pd#}L10Nhs$dN~toE6{#ARydx`d{#K2{4Q6_b9mI_9!ObpA$Au~Wf-PDYAae(
zvJ*Uw{;mjK2$(4YUc|^gNWUnmH;3qpqRhsJOPOQ-2JDAH9w}mKWrIM$S_*=k*^hC8
z){9m9VVYaqVIHB~#j9!`Ni_i3pQI`jGQ(tn`%jctQZ(^NhH5*AIop<K*<#OroHmrq
zFgxh>k{Rs>p=_0bNbzWX2hi534o2`QK%MH<jO>HOlIR^Yp)}82NzJ8IX?qjq?0s}m
zX<ga(p`)q322iu~myGPas(vNdEd4@hZq9ySaXQ8U(GHdBqXlzw$JlQrQdR=3erhOd
zG<VUKvMm1t%`{zKR%5<LKP_v`ycq^`76j;v#H*BEUSn>ej`EhwA4U?l0L~61ZY!T>
zen7{|=gk(6)c+qr!k0|{Euhx&?TpN$g%XJ$fNkyu^~2h^jdo3*+H@y)YDP-SSB0Cv
zwz?%~2LNT+CUozhw<gb-DE4$3_dv!~CmES(Oq?Q`U$NB`(LYv{<x3)E%}F+Wj$$2j
zcu_*Mf}G0rB|ip34IYf(A%O|o&UCt=GRsV-dn(IEx1tZmWYcn5>5a;cO%-77ksc;a
zJ4zTWUQTGk6{j8TJvug^RJ<e@Tha!wbn8%Y83!^>Eq9~SnL*cA<(pP|plbXGj3_3Z
zIrMy0wQ0Y(dVFSuL~jg)#hIl#I@MGcjF50363#MOQ$02Q1f-()IelnjUijbXqerUi
zOa+~&?u<VLPLkv{v=frsXhBWE=uv^9<?94#u%>g`)1ruVYd<cKiG#h@Q4^Z@zeAT5
z1Mv%_cAliKYMLiM1CEOsIr#-)t-ELrGSLdQFog3x+F0As^b2s^l+mt3{~&rCv2+=r
z1l`fGenxNB)~5X%*uhv7uj`)p@4~=n=05}`ioq=4wzHRRtXovE7hGo_1f<Yp=XY*J
zTdG%>8j<~!Hl?lY1#~5a@?NwPp}bdOC(BIKg@nC2VP_xRJZ0y~m&J~__euo+OJKrN
z=P<XOhr*N|j+~V;crY3b?O<8#r?vIz1K&6$m4eO3L>2QiQl>*3bskC#6!a$A!M-|l
zVCO-M9z+Q+ZdEZ&ilw@XE|ro1YrvW3JVg^5nu?B~KPj}&q8$d$c~-}y?>6L_eRNyH
zylHQUd`h{z$V^8ywK#tXDZNGn#rZ158)sD?13PIn89m&nog<0(XdT4pa8m&tYMj;d
zw&<md3Z|nLq(~*Z$qV8)RM<4D<9N!L@1va<^L>nIJn%GhQ5}s0GYB2s+qBudOQWY|
znNO)~YP<OZ<4ikd(X~^X&4=`}sk6;#u(D!jK<$|X@po<JQ)cT0)Y_bj%aWA|XD!)n
zbOe{1=8s_Nj`}Bo$i967FjKt){0t;5+%z&NzBYS6%*6}1!`z5&zOv0(2N0BInLsAS
z09A7LHt9EGF?XjT(IpEU>X3_JZwl<d7jsEMPHPBE>q)sac42gDIR6<VvOh%|^NQsF
zY5(T}seIZ^wYCi`r<sktiz|)^hm-%Mi7^q*4~{_F(0kLSbtC`gZjqFbsJ?iu`olzD
z1dxSTsrndshgEOxmb)6;oKTu;+b-QaeeOtm1XLydb{gj~oxYep+U%uKGpfytG;7AJ
zw6_y!ixty#Guju<Ofbw?D36qJC9i7dtjHt;Vlz{`krf<UA}huoZqcz}<7|60)i-yg
zWkjmu65bTi!RBf+NUt}~O1oGF9|yC=R64V5;hF>^*&B(zdXpQO%!AsR6mJaf^RZp(
zO?u!>HvMYmx6>rwY9&ALCXH^KHJsMW+UtoKpZ<DAE@iY7j2RR^P;=@>8r|8NJ~D`G
z35FP?^IP)I*rx+c2nH&o`&;IuNvY~U<%xmfXU{ZW(dx7B%dBDbz*21l>nOK1`-~^l
zUTI*jnwGUz)#=)ZoY553N4gCWY-AW4pvPJ(YNs%?jlsh0yQF{TuAMzQ`i8!|pl0#I
zOWr`1OQU+Tmw*-Q=#1>CXlsQ|1C;ldJsnUtK&<W9b7*6`-2xDM4iVC465nnv;Tvlv
zoxAzW0X-)nw*zu~sA1K}<14&%OWb8@UECFWDe-Vag7o>aR4Q~Px1)E1p6Y4gLTlna
zo%zP?JJxO4qBAc~dUQfNY3hk|+r8-Usk<|ySLfORMl{zzAe^h+3&&!=h7ddst^x_S
z!NOh@Oqg3{O6cWmZqbR>>r3#`vW!e?9-uq}?fHPY!o{s4_5s~GJMR4t;79b-?DBMl
zkP0u#b{Bmyd)eZ};Hf>yXF0Z<=oaS2bSv?KSD$WG*!Se@bv@l#P(PNnhX33Vbf7Ii
z#~mJC#L_Tnlh_{J;dHERg6(=_+AD20Mm6n)xyzxgPMim*lUl)u1uke$AMWO8u`ddW
zeHk5SZ>rb{*=m{fYCyFBFRavQ6w?_UJZdqObxd917KhWpI(Ns5g|$#q3vvdi54fDW
z#j@g`)JQ~C2W1J1Tch5s3cTx~C%ZD~osL4=t*6nQ?ah6#tt(?ApxWL9C=VigGb6V?
zX(@0!hMc)))9%h@+wGwL?3`%&=~QRcShs_Vr0+Z2Yq=doO!<jYd(K}KW7WHO2)N&Z
z!?FU*rD#iL<6!c&@HgjFm|pR)a8B>c4`uSQs?|ZUs}Am9g}_0C+U-Ye$kW_>f_4i%
zGpEqIoT0UpuByl!=C<e*XjIq6+#N%m(1%8FS)<)um1a9T(Y(aP3U>R&4Kbx|Tmh@<
z#&-dwjO<q#x%HkfKyd$aTR0qOxb?C}@E4v1bMuDvYh$~fd6&`dxjp<mJvH~`lB*!B
zqg)NOJu>z+fVT*|4)6|oZ(jb0#~Er2@1o54@iBKJ1hPCr?m6@0;|^k~Qsc^fkelvZ
zbjAEa4=+Ub$8=!+LQlB+==1q`e57SBm}wrO<qPts5laMn{GJHz6<CH%&mIKUuOB%7
zoR?)Qe2ES(=v**E>QT;MY{jNWX7EE%5O_-j_X(6T(RU2mP<1X7ix05HbXxwctpl$X
zp(`6ii~yJ-fwu`$;Qk2yD1!3N*CXwA=DJ5j_D;Z~i2{=C*l7dvwF0Jkkz2}{?BOLx
z?cHNd8!hjibk=Xd+Q1TAV;Xz9p?mTi<V9R_kB6WCBzTyIdm@pfKm@|lb27DuzUpop
zcfjWUVbFXRrDY!wNT(L2PdkqAI{8c_vwT&99rF$o%dSkMUB@{Iu2aCo{gCci*f8ck
zhN|a?;rr;_h2wKh4pj>Tp!EU87uB@h8)~`lg88Xr7(VGJCxChomTemVowlz{YWJe7
z#-s>|6cbP8czWpY!ep;yULVoxiy9~24}}>2nM=iOY5US1>WepwS{7$7%7naxALn(?
zHqKz^mh2Wu$^ISpxL?mH6i_DaagY<V?%Zt3Tb@1eUYJ~ruHiVv$b8JibN{axKmgOV
zt<>l+Q;NYGmf8~zhN;_?Olb8IKYM5(-4o3Bu=RVnbmfw&YR>?V2Z5e<7V__%!9)`4
zjX*O!JjZXPh08PO)RIfhYjo!de#7WOd4z=m_$cJ3$eQ^HU;{m{G@GUWb!qv)?_gV(
z3O)t(^m3E$5~=fGo{L)i^K*B<wh*8rRqdo&3!=gS!K9F8_Z_a&3|s=-KY*N~TfW^e
zfFoW~B=dIPPbrlav}GklAGF+$pz{evv~(K;LM4if`#A&mi=p+Z+K};Z4)$!5AQ+R8
z>Nj*zNqK1=9tAE6$LfLS0}MQ|5MyLM7Bh0_d(E(-McW00<hm$YZ`S``z$J31bT3Y&
z%kl;S|0F<IOHzAsv-ZGqaoBqEk|+BObM;!F`AyX>>%eRI1|3}oBZk5LxgaCxxn)_t
zHyU^h{eIbavy=`kuFCdW!5Ib8&cx~o>-jL(bGz@=G0%OSHm!<J4$Al$h-q>EoRL=t
z_t*Cd_h>1CZ{JE)J-Hcj2n4tN(CWX?xbr&lj_|KLp~?{iLO!`W%NX$2)I+Nq&(fm>
zFADbvrssW!{`tHHJ~=*JQ9$EYjG|lCjHLP%?E_vNY^~eCGQ6TdE|V4ZA{grBuOj$T
z1YeHeD-69GMD4!;8*~<jA>lQHE(N+82>XM4wb1gUPgYc$7pP=q+ad{-ce$830x2E+
zXarx2;Oh~5gW-@M9?{{Sr6*R7KT~dMiJSea^w!GGkw=rlca$1e<qy0WnR_dOzm4GA
z5tNPksJJP6vK-xZtq2J5nA&#(VoUIv!_5=RMuRY1Qxb|eoR?Qtl`#Es)dF*j=CAHp
z>rDyrg8!sAwCw9)<bE0bJ?LwY-jCq#BZw_15Wo@-_RbFgpQaC1=Z(1v@E@31>Jd?V
z%>?r>&04d9KXC0^(;g({0T~aAEim`T2>vO8pGNRAhC`APRQ55h>>Bei_4Ev${T0M>
zU>ZdqnC9OP`Co1^6S>oRClF43Ov@*-ZM<B-@lNm;ud?ZkV(HAf0KD*b2|z?!9<<&m
z?%pQ-!B?&_?(t61b!%&~-w7XMa#Tdy8+X6Bws2|%jG%bMlI(|A(5zj=)PW&6aaCqk
zxJtjIs&)MXCm|`X7zg`<Wy@601eB~f*i5Wk)I#*E^l_ehIB)!vQ&@XWNH@acic$H6
z&AOi3vb1~;gGjqn7~b)4hH-2Z&SmJv3C^*Sz2-}PnoSv-p&hs=dnbcwI3sD}`tvJK
zireW>(PU)+$^*n12N)&G&!I2Ymk#rD;2%GzDmP>e?1#u)kRA|z#$ST}gP(P71su{V
z$@Oy+VrnW9leQSes_;<QS{?Fxoc?l<)FVL(*S|BCYBo-wQyVswIuoF%6OuhiQ<4vE
z(u5jlpf@MuG`QhsV!xq;Tl{0;#Ljejx_8+yza^ONq`o4ZE-FUrLVqN@9Qu3s&+h~Z
zo_c^ul0jYjO==#!sNvX0$eUFUg0_FQl%50*j>p6~zFuAo30k>%I6dFzpQl4g>I%@Y
zN32M`;E1&WM4pcN<BK{XrX{#&`{zJNqLYYV9!GHdfZvE7t?hC^4di4%4Wz7`)Y@Lh
z-F_3u`jo1do(AdG*D0nNl=NB#etlRFDB}!%>7hHRj-9-qj->;2>^FvWTt+K5ZCmUj
zgnpxhqz2mRvuxa2&9bzUl7FEGG1zk9TI_U~q6-rhFqWz|=Xf7-uRoi*H)onFXw&At
zfk6qR{+5Vg&7~MtmZjbS7olXL?-2gA=+;Ox@UP*KE*5vp$6~51Q3U!ZlJs0R)QE0E
zFhcYChc{k?5X+7hgMYEp2@_gJ^6>!A5{W?U!(dL=_ZOH3I@Djc0wtu5JD9$?R1Az^
z=q_SnOLb^1BipX5YoC!n$X3Ps*lD%OO!3ZdMfX0MaeiK_nn(LKbgQ8<v<I04*1{B4
zGi%6K*na*MW$UK4f$(tcfxstWYc01pT}+*JCPAt@05#RJ4pYnX!Dxbrq7=D*IHgjP
zgmNq^E0B6LRf-nQ8NWqhg$IySs{a`B<!?e;>>on&@u;w|AItZnaIcgd+QHma!_5Zr
zF;?^{aM=yZjnh*L$LTljF-eIIjbl04E13jk0MF!13)%<JM!eL?q_2|jREL-d_k*59
zpgrbUzR=0m0Au}qXE-(;$+nDQ#galhM1{rV_bN*?VjpokNyC2v?X}>&6qZ68w~Xn&
WV4W3wk>_vUXl&cQi|#mo^8W$^(S&CJ

delta 8122
zcma)B33S%gmH)s0_NC+l!GvZZ;R|FV30VyZm=F>|fCM24iy+wuB<zVesDQSUo*C)j
z0EYImIGt))!crE|nW>$r7AVRY9IDiDL_I?-r=4?VPAed484<1Xe)s;rB_Eug$vL_C
zz5DLF_r81Yd;j-dcKlXdcvrocKbCHeosrUH=$}!JCaM`Qm*HHE%x?PL*mz%n8S`j$
z`dZaU@1>V?b*Dqnp9#7VB#>!osv3cf0Ei#N$B2h70u(C`0g9Ey8kybMpsT^fP;(8)
z6V#ucNSib6RU7Epj4ZW~PG=k~Z-<a*=>TkF-Agnww=i4=xGf8`R}-TLsGs&`CTTrC
z%N(7%%Q4wwqh4HI2q~ihV!MFy>wDJWuWBPRt34aO7!Ipm8-~zoBrq3N%zgAXS*3IK
zry~f)GayF2W6tb+6v#Y0PE!T8c^KqKrlv+R2vivJLF)Cdc~lQt>J6fAWY?)9)R^5`
zd?Z={WRFD;$j}Ux2=0q?IXiRAOB#x9FAZAva_~&nXC9}q<0{l@Y9CiIZ65|3IUsPv
zkd$u#l*x0<1a1OXCjW#+=DsY>{c38SlVYmJ>Grq+|CW$Ga~n;_DarX321(++4Je8G
zOO4DeGX8O}we*ghlu`Y_?6s{UA{`>trmc*m%Q-Q_FNG2*<wKw4l%;VB{f@buT{pV)
zXh!CLNl8#cZjpMDp3JRD_*<xz8EpmhvBaD7j+S_u?7S%n?1f0|fW%Z!VsYLq^$Z=#
zn>BSO*fJ}&?BkNy4X&Tz9*xw?85|(43pIdFU$DrC?i)X`{O`aMH9z2P8Spf)(a51Z
z1So4NIQCiEKYr$zAEHB?e2$?wsiB&riIqsP`8_I;Hs$A}r9gmJCnwpbqf-KwUcQ=G
z0Xmz%wE7?zqL7UWMBy4vNVk>mf&qtA9LPE^PgXv4732;tMKAOh16ZZ>d_mm`w#*?z
zYOQkJy%gPgDWVPUta7w>iaUVwLAVmIps>2N)v!3*fsB<AbfAD53e!|6ttm{3g+*3r
zRZxFnp(>}-g-Hnkj_3%eVsGY)KDu6*9?Ky@bgTwSEt(kkM@U7?o3}Ac418-5Jz7+v
z0(7`&df=x~lAUOWBs<ApoIYH60}Y?dkfsz*pY#e3#1c1;Gt|VwZfJ=LDTcpCmtlkW
zc%M-()2ZUhyq|;PU`AG4dT>cNXs$;OSGDmP+K*FaNnQCFaGfY?PokgYE!M>Q8%Ny|
zTd&f-l4Ac^9xJx!!;;1^uQLPI)H#Ns0#UPd+uA~N?rR>u1zc+z1h@nwf7{XKie{!n
zq@OO_S6llAx*~!uiy|2GA8_n=aq@5`!9dG|t!>m?y1wsC*2C_-6^0k1v=8XEbug%X
zAnYuc!GW+fUNo{)U|rQfkysB8ikM*^Pf<p}#!*%UX5`SI;e#O^UT>)FZOMZju@1nx
z7d5~L!=ByI+Gd0lb45yvTmL{;CX{EsgP{?jeiiLtFs)a`CRLWDs%^BmY}TarSU#$J
z&S|D4Bc)hTZ<+<-73;s#hh<fnAAl2Kjk6Nm;;pwNK2%e_ru^3|8D-~v&9r0;7vXsb
z*&v>k_vv@#RYku6C&J1Vv_n>|z>0FglS1sL=85rYJ1w8MQvHrDPE1r+={J)S=<A93
z>c6@DDYx4uWvV~WUr(B<`yuruJu@tUCR99?s6K%<*}y*ql<&Z2^mavpscz8kD<(C<
zO*P<v-h_xq|1Y3Oe-0>LjawSoHu7(rN(UXHf7K<B0XenYkdN&jX-8$lP<0zJvQK|W
zU)7|+ie7vE$%X11RZgz*zmISk*zs(WzB_qZV^WC0+qW?kLreuJ)?=Dsh&0+sQQmN2
z*@cqsFK9<iqB5wYs-7p{>2O27B+~J!LbaYQS5^5}v*~X_sYzK=Y8&qlF(Q454LiU~
zOxzlZVfRP*qHtido7flAW?zQT+fx?!?+NP|4qs?{^$=>U-sSS_e6)3P3dPl=m$b46
zIa*pg;7OPx!=vG?H>m`T>{eP?lNR%sSRBR{<LSpWGyO?n!DMZ*O?^TwQ;#I1h1p}m
za4aR)Cdcd%Es3lpKnrRMN?M})k?b&2!hjO?{6Q@27Wzr;cn76o(!bVi&BnSh6z3GP
zlEb!{3z)*(JdNyQv}t<4Jr4K+JwH7+ULd4`2NW}#E>B-Lw+KAZ#~<|E!3)#&s?_z4
z*8Wh@8U=cweTIwHWUhfDynT)~&qy0(zaIQx`7sT}TL}EKU#BxOMw|8-x-ui*v`^8#
z-uU{k(hi<OnHKb%DhK2ng*j0p`&3kg7)!u?S0Y`=k)A-CXO@re)_kLo)l~q>94i5%
z=XizwXQp=P3dPh<EVi!%=ZX#0eup(wVVG!`0w@kuYotd#Qa@_w8o=L+7x%Lllj*tH
z3G_yNhG}1;>-EzrYqf~%4dygJ(NPB|RXJTF`&zc9a$~~h#pc9)K@T@nn)cUpqG61h
zK^Gee;_R>W*QNUrEn?VTXKJd?c*AEsot2`YGYljKk>ab8+JrV1m=OR|e?w2t8n33Z
zht>mKlTYv@=RklrFS8L)9Bcv<2b(o=(orCM<x$w;>{~SOK!)3^p)sGT^Alq1TQUW@
z`oQv(@q?X^Q<-ee+v(xi`D(UyqH>;nO%Hd{*^P&wO59isC~mX>axIx}YGhw?nE_IO
z_AT#YYhTN<blaSY+r)5>>7)yDwq~ZPMfC8T4t){0IOpB$4k!>~OEhxkunWro=Q3Ol
zxR@?9ro|!^63SM(*%%nn9$G3vZdOwuVI^kF^)6f-_ng*D`p&d?TGw=sy9(_Uw7IFt
z<*s@3pG~Q%oo+QvRtKrPIc*XrRd$2F(8Atsz-KrohbM=HruiV)zpV4%s$bHM=IOHw
zcrzJ+K0mm!q8>wAbUq%28yI3Aah_rbf}vIqYaGxT<EeaZPY<8l!xvlLWmP6e2*u^8
z#--7NICpyRTVaR`qO*&K^#Se<6%$_vEG&Fy4~>|YsmiE)-q?Ge*BR_UI&^hOxM|J2
zyqQP^&)?bSntYa)%7WL<{!m^#5eRe7f#@Fka9(ZSQ<zN*Mjk{_nFxh*P!q$?u{;C_
zpB=tSTX7n4ZVkU2p??bjGe4Ag5k3H}m9B|%0&pjc8w3Jn?2+2!7_@hOQr&koLv&i~
zL%1F7!-2tOyg^WUjBd<}r+XKq)NBrF<7qhm6g7?gy4&bLWP6tZT4i^{<>3X1Wf4JU
zDNUTSASVaAz)U?;gjjt<KVMLm_cR9BXm8@_a2vM{wJFM%vo!j_<mMre=NlUis2#ma
z(H6IOtBI(Ny}HM_vn((`as;rSsuw5Imn}(s&Y@s|z`Vrcs78ELb58%cAV41THI3--
zXr>g@+3232G0fe}H;l1bFj_`;Ir~9A0J%hM3kwRJSAgFEIR)}duAA31lwIT;m~VOS
z1Lj65Y#m7#7jCNEgE^c0h9Rr_d%EqdyYGjgR2|DA%Fb1Wy8*A$)<wx`4;@;RtM<~{
zi$<*-oOkDdmijXxxMNL0>3}A8PTUI);v(6022irGxaB)P202O_9-7dHOCe`U=6*P;
zWNx9&t1$eA;Jkn_FCo-XON?clm(l&x!F4O6QMC>}rX9Uq7_HREyCzImRI1;37t*L7
zqXVw@vFo^~bK2BR*25c;a}#Q$dh3C31b6m=d=4o#X4K!!*8e}^vB;yd599;#wWRiW
z4swLBs3g|-5I7%#yrhZiM9%hZ4&1`XyH&lc|66w%BkLg+>%|=oOXui?mPDWPZ@?Gm
z&6XrJjGlS0FzGfJ=Ry9YiO~_P>3&_))0&-+(DN*p=U((nRbz%8#LDp?;^e^rppP)G
zr5srOWkF)~N*TH=Wh8%B<Qg41{{D#m*jm@EFASj}yAU;gDYY6juu9pBBVdXbC{Yh`
z2?+OCn2VL;ecrI;JG&4lH;;bQHbH;SK4?#;&)bHn!{lpk%5gq|>CR<5`a0yq-iyp&
z(@2)#Q2nAnhC7`(T*lXBYIvwHoSUGiLbsA$YoDr4lG{<+$6<6Q@R)yrgt+>%FvNc2
zapi2zvRuiLVcaFQ4ntZtXxQ?eEi`b)qZtb7KkJ6A6rJy=9=basw7Y5KlC%+LAS<5y
zf+0Q88fbEMv*~l_<MV)7%$-d5>+x5BJN2(~Gq}HEMY(*KA0jahidbdzlO@?Y+P_{h
zTb-u7&bragRWH)`!_~njBL`<rx0@EWmHA~qya>j(=~tbpBPsxUpj7nFrayI#R=t$E
zbg_DaHZJul)m_fMV^{Ddb}0<s3qw3_cmllXM~2v|)YH0Bi`0Km)w1un{6sQ}9_fhB
zGE%T<@tN1%k7&rV)KH*aUGMno?x!X9CsShAJ=N*Dskkx%x^o?RgHOPK2phk-y7+%Y
zFZZjsOwHssTK6b*b`>QL1n+LVJB7C}-F>VpLqCfCsw>eaPhKf>y(>XoCSUiePF{|3
zQ@|=VOpeV}KuJ0RZloYz;pb47cML3F_qDtAV7a^ea%Z2Xx4Yw7++RSgu@wY2G<RRn
zTYmhtIBEIZD|ge&z}_1gkPpjT#QYk$2ZB4$A85+*)%ge5>+rLW`6&j;CFC=}h=g3C
zOUuWNaW5f7@(Rk<bzU|?(tG{xr@)F-c`?MkV(^_KKbX7sLc(D!BF1gbC5qPNEe9TZ
z524!uqkDpLxuN@%dUT~>c5hs@{?YXv^va6I7MWjSj9hoV0+hV)MjSD%kGal#OyeLH
zzV+KD(GI@2xgX0_@B0n$^uv`4W85!f4s?5Ers}6LtK!>xA&<4|!}rg7mt)tlk;sEt
z@KMtJMAShLm1@6$R2iipyx?zhrSfQ`-abkF(-Q9OfKmCM;7%mZQuOMoK*2T*d1q8N
zc^F3$MtvrFpdh?)-KJwJMpO3c<~|pplMAmE1IXdBz5&SLvW5Ugm9Z~H^ITMoFLiJk
zOV7vLEw@liQtbOifqgw#0Vv?f`ZkB|d=UBHtBFtMofXVtT){WItXn=RUDG?4FVpS~
z4#hBxlo{Lu$aQQD2Mj0NSH!7?F8eyjNv}A4MUoKuY)yfCLie~|>4<;R^p#Wf+HPM3
z$2CC5*CzMHhLXUCHs4e&?ZsFFU$xe_p#(fH8!4gG$_<7SQ#)9R9MB|DL63?NUEY#x
zIAos`JuHM8@!^$-pSk%fVxRD4(AAT!;%G}x$zoI_?p?Z2P~6^)WQ2xJtS06RO}sjV
zR)@XzY2>TWPH@XUDOw>3$6c%|-+X$mC!w@q@Em*(LP%abP$NEkSv;M=v<;;T>+1dw
Dq{tM8

diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp
index f5b55f170..9cfebfa16 100644
--- a/src/kernel/kernel_decls.cpp
+++ b/src/kernel/kernel_decls.cpp
@@ -65,6 +65,7 @@ MK_CONSTANT(congr2_fn, name("congr2"));
 MK_CONSTANT(congr_fn, name("congr"));
 MK_CONSTANT(exists_elim_fn, name("exists_elim"));
 MK_CONSTANT(exists_intro_fn, name("exists_intro"));
+MK_CONSTANT(nonempty_elim_fn, name("nonempty_elim"));
 MK_CONSTANT(nonempty_ex_intro_fn, name("nonempty_ex_intro"));
 MK_CONSTANT(exists_to_eps_fn, name("exists_to_eps"));
 MK_CONSTANT(axiom_of_choice_fn, name("axiom_of_choice"));
@@ -95,6 +96,7 @@ MK_CONSTANT(imp_truer_fn, name("imp_truer"));
 MK_CONSTANT(imp_truel_fn, name("imp_truel"));
 MK_CONSTANT(imp_falser_fn, name("imp_falser"));
 MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
+MK_CONSTANT(imp_or_fn, name("imp_or"));
 MK_CONSTANT(not_true, name("not_true"));
 MK_CONSTANT(not_false, name("not_false"));
 MK_CONSTANT(not_neq_fn, name("not_neq"));
@@ -108,6 +110,8 @@ MK_CONSTANT(not_iff_elim_fn, name("not_iff_elim"));
 MK_CONSTANT(not_implies_fn, name("not_implies"));
 MK_CONSTANT(not_implies_elim_fn, name("not_implies_elim"));
 MK_CONSTANT(not_congr_fn, name("not_congr"));
+MK_CONSTANT(exists_rem_fn, name("exists_rem"));
+MK_CONSTANT(forall_rem_fn, name("forall_rem"));
 MK_CONSTANT(eq_exists_intro_fn, name("eq_exists_intro"));
 MK_CONSTANT(not_forall_fn, name("not_forall"));
 MK_CONSTANT(not_forall_elim_fn, name("not_forall_elim"));
@@ -134,4 +138,5 @@ MK_CONSTANT(forall_and_distribute_fn, name("forall_and_distribute"));
 MK_CONSTANT(exists_and_distributer_fn, name("exists_and_distributer"));
 MK_CONSTANT(exists_and_distributel_fn, name("exists_and_distributel"));
 MK_CONSTANT(exists_or_distribute_fn, name("exists_or_distribute"));
+MK_CONSTANT(exists_imp_distribute_fn, name("exists_imp_distribute"));
 }
diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h
index 459979b38..b789acbad 100644
--- a/src/kernel/kernel_decls.h
+++ b/src/kernel/kernel_decls.h
@@ -188,6 +188,9 @@ inline expr mk_exists_elim_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_exists_intro_fn();
 bool is_exists_intro_fn(expr const & e);
 inline expr mk_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_exists_intro_fn(), e1, e2, e3, e4}); }
+expr mk_nonempty_elim_fn();
+bool is_nonempty_elim_fn(expr const & e);
+inline expr mk_nonempty_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_nonempty_elim_fn(), e1, e2, e3, e4}); }
 expr mk_nonempty_ex_intro_fn();
 bool is_nonempty_ex_intro_fn(expr const & e);
 inline expr mk_nonempty_ex_intro_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_nonempty_ex_intro_fn(), e1, e2, e3}); }
@@ -278,6 +281,9 @@ inline expr mk_imp_falser_th(expr const & e1) { return mk_app({mk_imp_falser_fn(
 expr mk_imp_falsel_fn();
 bool is_imp_falsel_fn(expr const & e);
 inline expr mk_imp_falsel_th(expr const & e1) { return mk_app({mk_imp_falsel_fn(), e1}); }
+expr mk_imp_or_fn();
+bool is_imp_or_fn(expr const & e);
+inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); }
 expr mk_not_true();
 bool is_not_true(expr const & e);
 expr mk_not_false();
@@ -315,6 +321,12 @@ inline expr mk_not_implies_elim_th(expr const & e1, expr const & e2, expr const
 expr mk_not_congr_fn();
 bool is_not_congr_fn(expr const & e);
 inline expr mk_not_congr_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_not_congr_fn(), e1, e2, e3}); }
+expr mk_exists_rem_fn();
+bool is_exists_rem_fn(expr const & e);
+inline expr mk_exists_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_rem_fn(), e1, e2, e3}); }
+expr mk_forall_rem_fn();
+bool is_forall_rem_fn(expr const & e);
+inline expr mk_forall_rem_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_forall_rem_fn(), e1, e2, e3}); }
 expr mk_eq_exists_intro_fn();
 bool is_eq_exists_intro_fn(expr const & e);
 inline expr mk_eq_exists_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_eq_exists_intro_fn(), e1, e2, e3, e4}); }
@@ -393,4 +405,7 @@ inline expr mk_exists_and_distributel_th(expr const & e1, expr const & e2, expr
 expr mk_exists_or_distribute_fn();
 bool is_exists_or_distribute_fn(expr const & e);
 inline expr mk_exists_or_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_or_distribute_fn(), e1, e2, e3}); }
+expr mk_exists_imp_distribute_fn();
+bool is_exists_imp_distribute_fn(expr const & e);
+inline expr mk_exists_imp_distribute_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_imp_distribute_fn(), e1, e2, e3}); }
 }