From c01f82aeb71fba114e946684cefd94ff21112a33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Feb 2014 23:04:44 -0800
Subject: [PATCH] feat(builtin): add sum types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/CMakeLists.txt            |   1 +
 src/builtin/obj/kernel.olean          | Bin 49327 -> 49224 bytes
 src/builtin/obj/optional.olean        | Bin 6810 -> 6683 bytes
 src/builtin/obj/subtype.olean         | Bin 3049 -> 3026 bytes
 src/builtin/obj/sum.olean             | Bin 0 -> 10414 bytes
 src/builtin/optional.lean             |  16 ++--
 src/builtin/sum.lean                  | 122 ++++++++++++++++++++++++++
 src/library/elaborator/elaborator.cpp |   4 +-
 8 files changed, 133 insertions(+), 10 deletions(-)
 create mode 100644 src/builtin/obj/sum.olean
 create mode 100644 src/builtin/sum.lean

diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
index 36ff51bfb..17822f71b 100644
--- a/src/builtin/CMakeLists.txt
+++ b/src/builtin/CMakeLists.txt
@@ -95,6 +95,7 @@ add_theory("Real.lean"         "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
 add_theory("specialfn.lean"    "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
 add_theory("subtype.lean"      "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
 add_theory("optional.lean"     "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
+add_theory("sum.lean"          "${CMAKE_CURRENT_BINARY_DIR}/optional.olean")
 
 update_interface("kernel.olean"       "kernel" "-n")
 update_interface("Nat.olean"          "library/arith" "-n")
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 6c1b816f472ab11adfac0a85f132c3a9d4489623..9b1671905ddac4f63553e336b3ee7b91423ee4e0 100644
GIT binary patch
delta 2180
zcmZuyZA_b06n<|h6#Bja8lhUyQlP8|BW$`XDiN|_9Qdc%AaTmvI%Y6RoF+4oNHAOC
z4_y{BJsLA2f-=6w7|=342P`orV{FmD5~dLy{t_`J{%~jp;(5+nO4mrzC+9xrx#ymb
zdtdrb#a%lYH_-ECyryY(qV%u+RJ~+tKf&18{;2vQ)X{EJ2~+S+Q}BFK<_w$G7Ob!5
zGg`74v?Z)(=(&zoC;aiNaA|h{8~n51pp6c{x=H>{uewfeb-vHI-kGIl=#egW;cRRm
z?0X&imSa6s*HxN157#X~Fy@@!Xu8X<Rw$+0tCne3_c7-$Ue;+j07-J04SOim*Zql7
z3AFb@qjH3%E>tR2M2QzaezMeNse@K8lYJ$5alEje7OE6HK(m|lM^QA*U;IE-(o219
zu9`&4Uh%MTRLg^z&Og0|oR=PdAlh3YvO}RmmwZYcr}z5nR0FN_f9+<`9-lZP@&=A-
zQVn!tAY0YY9|NzdMmjj?)1%~cdN7B5eS=L#jg2E%e=v{U9rWZi3-J?()@_UyG*WM4
zumx=vGnqDO3}!k5%*o_bIfUvp2F~9TddOInf>J^B(09R1M>m_AJr{^(F}oJbRRI<k
zIYJS!W`{3GheJ*y2(2A~^<Fv|a;qS<hPI_`mYU>@D)sx&0cRWZI8lp}3Vvmav)MD0
z&h2`BC`)}qZx8L@s=J5wC7gltUHWS%E1?PI8Opdkm&&m#?i<D0Wyx_kH{7Owpj{#V
zaE9?ao00T9!)bIj$wp^~-Bp_jqTl5Z!KgS|8yy(5nJT+#kBRCo?g9Q5B9}p{m+}Lo
zM$$3^@Zol93jo<}wkJS4M$!^$z%G%eCyfq|q!gKRU1v@=&40H{yf*zVx)jepHmP~U
zo2~y1d)4eXcsZvYmW*tbejdr>k=+|{^SjR&EtU(Qq{gLuR>>>pma8!r+0P|A^j;>z
zezpu7eKzWe+JrQ;g>Z>CM_uBIe-Z3PbiB3E+}hj1GKBqX83s7yXCxOe>Jg2cDMHa0
z`lc}4bRX11Ad!M8Or}#~8Cw~I(+(#$IA$hie~R_0JUY2MW0m<b^3Czd6$aze5)nO#
z!E9g+?H|v67<01WBH4l%{{3(N!|@DHfPL}R4Ej3^vQ?_oQp4F?8+Sh_GmXaqMve>;
z#~Qh`KJIzUD?~DgJl%3)r>3w`Ln6uvz=y{GXKmTesLzvs!nG^F=Kr26S3vHYnE}Qc
z7SiVv#f6JzUWl~Fpq^lmw5_vjSZBqJP5L6;oybZFBw89Ek;dz{$a^KHDggJ74C)yM
znUi%cGF2hB+y=&AontUcppJ_SbW3QI(77w0s#mCZ^68xcsLV3(#kOFnH%G>(S!Er0
zcYKFiCSA|Ui?YfmJ{<yC*T<}pqj{|g5KrwBB?hB8#H6)J7k_n}Q~6E_Ag{_UQSc9k
z&#Im(D>P$cSF{UjG~Vum-iD~GpPJgeU2d;b6n;SL3O`s#Ezw^a@=Uv4c$rzl4^;tD
zPWqO?tSGiZBxvksFgq4q7CZ;wks=VssG>JIT+}=5sFo7s0~K4sf~0gWvJoX22LVUG
W#ayke?~ZYtQm-CSx9QERW&Z)&nR?X#

delta 2346
zcmah~TWpj?6rS1ccDMWgK%15|+lCf;+oh$pLNFo`0)-ah13`^de9*FjC0inqgkTK1
z-jxT99w5G8D9{^%z5J!L-Ikh|C@+MxXqpHiZ6XOaky!CkO{AXh%x=4FOx$F@oH^&4
zbDJ~sUx}r4yqVV7-qcv4l**`JQ0`&|-?WH;sF%V0psZn1>wQpELY%-hwG`k6qyZ+x
zUd58<?tj_G=*y-l?a-;y2N`qDtkf;ehBIEB{ta*Oe@l;_J(4%VqWdJ)qhUtZ3I;WS
z^$5+hET!qQM+4w^{)AbL17`T||BgOu-l4yzJI%#<loqvoz<8piK#x#wOMdzFh0d^V
zKlV*6v~ZXWc{gCX2^d%q=T~~Bb%*yJ>ho98-R68fMORxRfk|mmA*)TgQy|2hnzmzF
zFQyyquj!yucW%4ZYpLmrPuJCWU3<Z`YE5fP&_VZ6QPn^XP=2HSBt=b)=Redt>5ucL
zf)Sr<vshTDSF;_rBGhqVO?Ikvo6uf#e!mdX`VcMa*sEjoPRG~zOxhGm`Y_I7?A54Z
zw5M~0j?nv^`}Es1)fuu<=v35I$hMlUBX&dv<p*}dp|5o<-*j3Ox1eY(WprJK*v8=P
z_PR_mZC=-538N-J(R+#*jchegRd)_M-`ZWIyJ%l`UREcJexaaIRu>&-TLblXSFDLk
z<(a~OZ6GAQ?0`aMLsyF$OFv>+4h5ZjJwT5*r8&tqWdu^{e#LoW71CAWHBHL7gPo?-
zpIFQYh;|a%82#cD=&O|3Q^i?t>ZwgX2K9UNQBOhoyAY3&(=(dMv9`@Sr{fo;h>Jz5
zjpM(-y(f<UW>KX{_cTOgV*LgwS;OMqb?cJZ<77}JXUH+?cc(^y+SI|O-4S8kr&w<=
z&;WT15CupyZhlA7gnOr=VFtN}e7d)K!xbjge^{Gn$Nf1GSJAqU0zCX@k=9%)-fW9J
zV|oucB_>!imh0eZrD0bY010gPlH&|@oyqo^{2X#FRZ8k|u4*DRzv)ZiOotsLOf1<;
zsH$%{kIK%zoIE)5?3!m+QAw+TVtp97*ZY?>M9Y|AjWfvj$Oe(@9O%$1J20Ok@q{QG
zJ3C2CbUwsuYY<9w$PfdR+n>92VM-<&Cix#tGG&h%n{Uz8sdc~FzdbCofR_M2KmRcc
zn?uUSqDR__d%=e|*^gUo59F@LF!(kysQt6ghYm=xlGjt%@D}XYYNjMJ(XaY}{0C$d
zJP2Ty$)O{xT}~$kmOs5p6pNv#;PZVb<$QI3wHnWjjn9kw<SIrBZ>}j7Ju)*QZ-bSR
z3)%5}3n%O`xzXBqrG0z0HP&r95D%t<z~aa8f+Y<;*I~Gmo?AC*C|>v^{8>LT=q)he
za=1rl4^)(MW*d3BM;YvD29-8@mUBeAnpO`U*DuqR!N;QTo@f=`b{Ce`=`h3<klnJL
z?YD(PP>7xYh#A)yj72`n@~JiJD4ZtNbYLi08u3Aq#s9<xEagI%6+y&T8sCJWa6m%I
z<@1Y|LSy=QXk)pUWLK&Q`_UeM2z)Ohv8%ev4`<0R3qLWK^!er7H|7G&JsVQ6-N;+*
zItEqtKLsK``&lqe5$K$*Wsvf0TwgOB@MAv*vl<7u6|LO0h_(!8nL_0iNv(#W!@-gl
em}$QRzC4O%oG~zSuabR;+J~Rl<CO8$#(x1QxrTxO

diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean
index c4e092fe2b15eecf53c4f8c5f4576ef34651caf4..ab2fa979ca4e1510a66bf2f663ce9aa4d78d088d 100644
GIT binary patch
literal 6683
zcmZ`;-EUmQ6`#3l*bQ!#wlq?fCc<nIdrgrbeD+i7ha4QyrqGm%pqBNu_d33?zIVNQ
zO%j!U01qi33KB@P<pts>YE+@BPwh*Cs;c6leLzUi@&~k!RsVzb{C;QV&g|M*DdTfy
z&YbT#bLOTTWNERU4>IF^Hs2hUqsly$jf!kw9Cj+LJUHH7tu72R)6dpTQVy%UEYd-5
zILi8_m3-aYWKHs@KtuVLngm=M$v4V!p!}02{#qgg8vq+e8%a4bvgJIt*dvXkC@W)*
zU{$vWNp?OTSL5Dxk#B7~g>`L07pj4Mq6_3F)JTR^;Yj*ft_nkM3-QJg>O$DqYQxOb
z=9zK1nFSk30`u^*M=^dDL$fLR6F4TyZi#3?=mHwtr0`EG1;)={utHmodU;We;DXvr
zti>#4Auami5^}j2i|u0=4?+S}r<6A4Y%95dzorc}MM42}@ateub?Drd;|C@)f!_@^
zSr<?fks+X)0NyfRM}*3AT^)QJu$6VuSS>R~d1FCiMiQ^4@LyJndCaQ~fSTOKNovl$
zZSln@TX!j?>^R=aEd=KPegT6$xjDpN^C=(<EU^7WSxm<?gwpy@+D5XT4#t^No94rz
zK4hYV_l*s{S)vXLkRuEvm3w5;t48_Lc`AD-=@VSXa02NDV1Hh0q^lu?<sfh-ujG6g
z&Cr`bXe>qCPWV`3rp{%T)8ckvq}xE#z;J+$ypOmyun~+VN9M)}l|+{ti{qu*!Dm4^
z@Hx#*cL6l>4N~2au8!sG;-^vpIgX2fLrCrf67k153;gRNM#p{^JM|3R15oqmUO<+1
z^?V?xQo>DoE<y7-;wu1~J|pfHBo?2Kd(#>e*kDd$(AxC?K$Xq(I!*u0ank!#v-V(6
zTQU{|kT;RtUXlA{I!evFcrsh7Bvq;ldw4_KvOq?1YUFSOJcyyBCd_pnAi7~ItTURr
z!lf@`lUni>K$=ls<zzEimWrW!$@b<J<{4kIh}_#&?_>QZ7=DW3XmIzgbxMyb7&cHl
zElfb4os|mO8)d_>R7gx53<{7`qd_j6U?Zy)xpab*J=fc}N7*W;<w*!J<|6fG+H`^m
zl=uSHU(!gTmN=c;^v|m`PPr(4*%k`Vly2lStq>>M-A1xj7H3DSp2pCW1Z+R=^Qs$|
z@gS+8wPd}D7)x&M`1JackTh(RV12nr^J1;qBfBVq5$%V3Qk%3W;LJ+eaO#A@7$3wS
zW%E>IaUXM+FkIdhPRuf0j*=5)F|(Ff(_XIEnNH6FCCycibhqX*qjU!A#I+W@9z3Pa
zt=E_6nm2%Rg&uyvdze#8HF4xoW#c^xlDKj_oercWK?B5JD{*xL_nKx5j<`E*3|pIK
ze=E#>8=#icQvm;nCPLDmzqTNCMek+j{jG|{wpZTu19S+hWrx0!B#e)jdI@uX_SQTk
zNR%C}4DPChDK@!==MMmB!X=KZkUH@_QZa>i)o7}GksCr-O5kit&XJy~GI#sHFL~Wy
zNTeI?Qm^0SZA7zMWJBeoiJSqa{a+&;Kv&|vPZ+6+-v<kIACnF8P0qRW-dkr1dLMLj
zC9_2mpJt#3Tvq5G5;D07w?|@6F#8%63?XR-Zp<*N*+Qn8p!IF_s7Q=F!IZmRjF5Nu
zy%!`)3SkDZcABf>foh1J0H`tS0n!U$1>k!)zsG$k#?16>^KVR^gD;2UUaH-q>rnrM
zCC&Fo2nMCD0e^SOCm}=si{&PlnHo%*bMrI=MNRUWy#7TH!+$U^BbAF!qaVt2<UDQ1
z>Q@Uk$?0WSOv5{GHt5MpMYdNtN=)TPFay*exDIeue6YS<WalejlZFFl!EvlySB-`?
z+gkUBnkf;Su+Q7DhTV}7<GeUK$f~l~^)#ssaY@NC1mU+~*yr1Bz78<6K#?tuOhebf
zVC^CXYV#7cehRpnE{&`=o##f=2&K<{asg}q!=N`YBTwFRfMe(!(2?shU!QaUX;~^?
zlruGCM%e?}`fpd_^$;CihE%RoUqGxs(E_PIriGlP0!@h(-Y7WuBlq0oYPSW=OQ?Dy
z!6En0V}gRH*kW*-J&X;i10W5bwo$-el-pfebKe+K2rcB6E^39-L!3&syr(*<2RJOo
zdI)Y0VU~JyBRx1vrfqTR_`;^EXpt+p&nFf7o~hnoZKJHp&570%F_qhiC-KJMcpd|)
zaG6VUppp`p;;(zWX>Up#!xnXW2B5m@$AC`HCOnLK;cC||uNo}fAx$9u8gmxI1_pUF
z>)OL;5iv8dD!!KYnO1XpP5q%>LSoo&V#h@czrdi;q6vJI@g`Lwo_zKoT8AR*e}=7E
zz;^&@CpbsY`@r4Fm}9M@q<4YJm9fkNWFMN9=j^ao^rYo>%`ONo!q0nZ`a3P<YoOvK
zVfD^+eDJUhtmpuGs|)g^=4v0KL+EVHAX?G&?F7k}7D5zy^~26SCY<aU?q2~{(Apmm
zKSP{3a#AyeevKXwOvNM!*Aqv42b&jTnZ7f(s}Qk9=72H@ay3c|ZIJA0Fe@VTrclDt
z9wasc!zObAeYZ+MiL-nVXg<yfZWftD&l6O;s4@E!9=b)^iEMO7Qvy8FrgaXxLZ3#$
z+dz2Im*P(SmSf?f?|HB^zgl(HPWiz!7r^^N3|eSkCa5C9E)5u$FxVDG=DwD?S7;Jt
z(^<P^bH@z!(%KL|#kp(Zh)@MS(4vDzpY1?+hwF0$gKOQ>sCKPBgOrvBJ$R<>xuoc8
z&t-qU=SfnR<#jS>^h9t}LZw(j6MY537Mla7Vph5GBVagJpm`3gctq`UfS#vKAq9NM
z?V%u(7X{thLFnugWW?RHdIca{Y~LieS3Pdpvk7X1_I$2T)Q;i>WDf-eC`Uz{4YA{F
z6g%K5?QMA0ZeZ96X6*pKOd|T?HGqfJnnYl7rZs$=sxQK(w}m7=UR=2f9>2kg8gVO?
zo&$b`LeMMND=I_{gs6R-4F<j=xUZK=MFI?miBs4W<}@B6_6mmI%b-bBe;E7`=EH}<
zyy$Ps*O#)0-*XRRo7t2`>bPFdwE42&cMBPt6Vs+tt?>Q@h@x)~(5hdO1;JmD8NpwJ
z;4cK<1o+pcdpllZJeEV^@L)r%eY|#<>2fD8Dfe}tc7;J2yY87shd3EX8-+C(?wwJ$
zD)w&_%;E2{>`G)!*<n#(vBWZuh|=Ij%jgRG{sNX*l@|R~xEM@f9}h>_A=QO2ch>wv
zO18N}{ZY{8tq^@CGL7$m4-d>ggKBSqBUe5KRLA-aL8OQN&M-AISlG`Gei6>cVubr|
zg3**d_Bj#$i(nGfj+|dMYm%u?vUtv!m9*dQjYcMsZ>;I|po;&~!9R1Up`*i|-$ws2
ZvFkZ}9lH91&vn+L$K+DcKY{-c`aeHGeH;J)

literal 6810
zcmZ`;-EUk+6`#3lx^|6ZAfS3dO59CiuR|qB%V+rzL2__FO(RT!7Q}j;y|!<=zPsMN
zTkHqEDj``-Md?E&C?Fo1rcy#5`h?&GM?6)C7pMdX3BeOQBK`u-?|0_QYiFe#pP6&!
ze9xJgn|?3vl$%8_H|}SPok4$CnP>80nfHtvUF}pJ9gR1t{XuTJ`KHPGgR1D4onCt|
z%)4efyJYUSCVN7#f&A;33{q>^=llJh%FpWfYdIiV16n&*%lbnjOZK?Lo~>nNzcS`5
zsJcX0^1WhIjoRa~*d05Am3G7ynt^p<3-o8SNWg|jB>ya_BGCK7aqTQ^A#QB7ZKi^I
zX4K!wqmN{Pd-&ONfbRvU*TsG!=f&7vQ7r?8fDYHG{N2g{_#OZ&y!~OjD61ht5ZnYU
z6)A*H*_Dt`$|(>V=K<%Tfu>VS19Nsd+s9wifSID9ggN*%0n{7@ciPE=kf|u|9f7R{
ztd7hO(M3StzZfz?<4M;5Uj%N2E*7h2#;9x%G-qV-W{Uh(<ygeL`T(rXWt^ntT-%UX
z4D(G_QYwz{43`jH0Qw04du3;Uzvf*SFtHfTmHl!ur!ke*r_$E4%}#HWJG1FN0_syH
zM)=s+7@HN^umn9KKuWnyA?<2dJX>^R4K=-!bb!k!Hz0FiM-}CEXQQaxwgSz_u86ZT
z!rc7;#!}w};^%8qp|D+nOAfp+vT)`57}bwrqUOD=#RyO$3+1wEV*HK8UQ<&Mz_{5U
zXN`+K4Ad;v$n{WXV<a0HKh+A%Nn8dV^YbAL68YG4QGVEOjPjSUQa98iK((ko0?g8{
zw$BPp%D6~3DR@4>@jB4DFOP?1kg6|6?MVwtEHG;T+Q>c*RCTk~))>D9PWqT?3D1*q
z%6q{IPpp!X#v<5or2M^cACu{%c8l`q{CXv|RPCP-AyKkKL9(r6_XC{=*rg59WSk0y
zW)$hnFfG%_ej1$W-DiMlm3@|z^=wsIimsh;&7n{Ej50;JOn|=+z-@RghQ6VhigX&3
zwl<Jd6flyXo0Znu9_E9Qv`);<PXkT?kX187Db45`+ZfBa8MT~9Z(K+!S9Z?RkZjCB
zETLv}ff}C&{RPb+nv64~!En43#?*_hnD3$^P1r_BlLm3J(W+(F`{mY<ZPggMl0obT
zeT}uEFm5V!G-%c{is|IyrZ1~c2}{i;h1Hc4wkWSxCsY+xEYc?icMIaTIc7<zd)h0o
zl_g)CT2&nI3V^iMtBLckV(uoutz((REGy?6B~cgabA_$$M}f}DdJaSK+#zJ-wVau-
zCqd^}3-jd|G>vnhuP{nK!I%^V`*|O1POSvyB)BTZ2lorYk~WlQJ3YC!;F84ObmrO#
z&OR+3>~dG;%wU6VUyZYm1Jy2j4d`!i(U6_MUqc3=(YNzGfAWIZ@W#740|Ue~9)SEJ
z$4n!AQ0<@)`@MJRG0emx)V0WCeX@g<?q>8Gp!DM=;S(6^#8-i7E_e)Sy?m1Nn44XU
z>Eb@HB-~m$-nOrR7;VF$>+L&wQn47O=`oFy+vXG`&wY-3KwYc*I&su1es3>@3s2rF
zb~xv1{A8P{=uhBl0I+1F`oE0<E{m&*{Y~;Fr{s9pO`F2uL`v#Wnx;rg21VwoG@N8#
zlbIwEth;;V2*rorTQT5LN0>pbo#h&M3^hgTKsAR<wH^!`n0yPH_@Zykn3+6v{)5SV
z#BwldclIz6HB|pQqAZiOILou^5aYWOF=1F)q5lK9PBPmZi)Me3j-bg&h^XP;L;?N_
zKvgQmmr+}$li=ySEj(|qNVYKhjj8$I&BoxdT~X{E!cDFqx&^dGbQ|cb#9(t==6e-J
z*rR~zIIs+Wb9ch-#q(fy)9-ASL=3`=_aVpX#EDT+ZuRo2UmknI1V>y^vKK+`g8(!B
ze$HnEW|pXOnviAaZa1K@lhB$MXtnMTqU?0)x(0}|P;Tdz0GUKRnHd1eW&oT(cg1MR
z@mXvh4FGv5;D+p}0V~Qrpl^h6C9#Ov;o(T#&2S3w5|R+e{daoESsGB6T;VZ;jW2C7
zQd`q-eHW(QM|8;bi<qDy8nzt6X7!PRRWw}Fr`IV=-jLH?uI>KPOcTgRX)W{$XNNo^
zD7HmeY6sBe)D9Wj)0m|lt;7z_QfNbhI@;fH9W4n3*ZHCnb(436>)ZXRzjNdY>drLo
z#QS34UkxVQB546*X@MR5b+0_`b8cK(H6r}3G5~%LU~M+zX4GRqZ}jrw0qG&R6ymQj
zTL9Yt^14>qHC!1nbA&3fmWP~nb4E?$p;1C%*cGfe0C*8Vvqcy9dSl;GCKfhTXdg<v
z{{fb21AmQDVhrS9))=^h8RSFq0Ne$TBV!f8H}<hvdG`+5Wm~S^?(&QI1H}16OW)L1
zo`Z|!X7$W<a_|C<q8I>1s|EHfNVQKfAPlxv5WQ&mu0-~grI>|wc=Xw)M3Vgm*RMk=
zc<r}1ev)HoF;@uZXMkUdcCZvP1`EoM6*A3OP8Iv>y6r}jDTR8sB;VDrQ}Q+;Pg!VX
z+-w&ZZ~DP2E?YT)#j?EWERRR9j*C(FmRm?mb3w*tnf3HTqL5_#GZ6Tr@=slg4?!I-
z(`8)8oXb)HL%rHA$YgSxBjbZ${F3k0&G6`BXJc|KR%roFhq6wcCVdI;F96z!S@BI(
z5m#wO$pv7Ut{(%{UicCnrEZ4sWZiU*c_7n~Ei(gQmjDi^Tni6l%4#sRuVJjlEf9^N
zZl<9Ynkzzbg~;kNiUPx(Ob!LTli3?5?lg^9&)5C3>VbyXVx^fv5jU)XZ<Z*nvnrKe
z6XU)E4^Is(MU70bQ$_pxyFDFs@*trDO=QllQxL$25#ktz*<Vr`-a}5>Y=$19cS6@l
z$Z{&|Jw2w9!h|+^I+{i8s<;5@CIFH`74~&*xMxU#$?99e#DKgE${BSDCnnX?CBA4U
z7riblCfRrt_XcGA3KaF^3~gM%_%@Z`LSb*K64KPmN1>3VmU#IldCA2*VC-9Mx|VF9
zC2MbE@=PdBdz*UzFB?nJufdP7#7|z|!63d_in2SF&pQ1weI;JQ3bP|Ovx|D(Gd{Ou
z{IIa;{aLpJ52w5SU3n<0>;sIzE0Cbqk)HwE;q1=^vwtA^3!s0jyBFypbN5A!7$~S5
z?mhd>5M0yZ%I|~ZK0j!Hz}f|1JJpSiSaLI{6uF#X0^a+GgbR@UGqqn3ihUbk3ry6-
z*frUS*mprDMR{;e=6d`4>k>$8Wy}76O?GPqDxzh_Ocw=HMQ8=G%(a4lM0@n^!opzr
za|teITJ!&mrrm-DQvL-je1ra}4CH41_@HB^K$znv#$?PVXfpO+A(JWnj=+idKNLrY
zde7&#)W9<F5t#4r^-j0j9u7?=Uv)d<UX}izhkrcNLdOS_-$?#n<k%zo9(>`m(mm+O
N6LqERUdI1N{U2F{ifsS@

diff --git a/src/builtin/obj/subtype.olean b/src/builtin/obj/subtype.olean
index c4ee00afdfb7cd8801512ebe998f6f5c2339533a..a408f48c2c8befe949c5a735bd44ffe191870ee9 100644
GIT binary patch
delta 370
zcmaDUeo1@-Hw&ZnW*(OFjEqv7@38hV38*jt0S^<9U<0wHO|IvdZ?Ig0nW>~GF|QaT
z#K5ouL@26)NF@*f<}X$QG0VaH$$p%Y@teR*5P?rANPaO`5r~)uBDSb8GZk0n=7QKz
z!?%H0it5ZD$__*@teAX^Q?4H3S}-3(fDPITVr^z;ssPapd%(_A0C|W5;o`j@sTBwp
zL--&;unQKWs|3j~f-TDjF~J@Nx`_`cstyv^0T!Ly#1+XXKKTxp8oM>b?8yfiMJCH~
MJ2PIHoXFh)0Mq6*wEzGB

delta 387
zcmca4{!)AcHw&ZHW*(OFjErfU@38hViE%Oj0Xq|rU{eM$7lR1K$(0=Q>sM$nGnEu2
z<`sj47#LQ92t`#8sRSax{KaY@W;ucnVo8FCX<(KHh};Y!h}W(NQa+7A6G(1VV`eI@
z%*_RfK#kZAVkxRKgD5)?!LV}j0Zus+P7sqF%m;e}Y#$?tzYRoeVP~pfPyw-cKm=HJ
z@nl9W(a-~6KEfXmK1dMkg~bRTBV-uCCgp<^flUHCicuZJ-w76+oXr)<XfpXIml~th
P<TqTgjMpc7ad!X!_jERF

diff --git a/src/builtin/obj/sum.olean b/src/builtin/obj/sum.olean
new file mode 100644
index 0000000000000000000000000000000000000000..88a9321bebed9616885b6df68fa7178bbe0c984d
GIT binary patch
literal 10414
zcma)CZH$~%6~6b*es!l)YKtONzJ_kMTd3H^wF?PNcgt?K6iP{of@pSUyYJG0-I?v|
zw6qFZz|s;Z1;j{2NR*&IMU63j6!{_8s2K2vCgPu}e~J3f1V}v3bKdtoccvq_$(}j)
zo^#JV=iGD7{g|oGCzaY<bv|+FpRX<~)*DTCZ_=nG^Db@et~4`r>EKNB$YPQ;>x<25
zy;hlbv&ozbO9vOG78}W|>kFf<-@9<TU}Gw}FD$xcq2jJ8gnW<-Li3;(3Sq2XpLebo
zEp{ndKwHr+U|j=+P)iN~b*@_)z^_8XLs;nHhs@Gt)70v<)WG5ZIQsz#J%Fynu@?Xh
znGIAQJ*IuXN~cKzX6jAVsYEs^y@Kf4f_On)#CF$OwSWz1=t`KT3%+uTm1?8IWPRc$
z{Dr<SqsX#wn7*Q{GN-$c6rvwB^kYB+doLo|O$b0$uiCk=h=yA&|H1p_en+>if+|zh
z+C7_E^~qFGJJEtF_zQHLS_D0pq4P3;A}K|nrM@uf)aOPolU^nrKxHTw@U9-Ne^Ecw
zm`lK@E?)y|BTc*%=(R*I2fB&q6+l0|o(r+mbdhGmoOu{@8blpKZ)(vtQ=wburj9FQ
zNgK(W#3ueY_%pytnJX`rMwger^PIW4)tMM2J@8?=!06yA(>v?Yq)tWi8~P$wtB&X_
zYXBGZL)}EGx@jGF6deS13w<*LbT`orKyT%oTWxyUN02%PT=c^oHubR1$?jEa!7-k*
z?E#ki2E_AylN@eJov7c_(LEZUw`7qgu9$&H2cK+8g9&Y03Gv|M=61@R;0dZT{2io8
zwG$AA*A?)AEO3rJqrhlUk?y$$ZS~(qLq7>rU3o1~<^7bQn}F`4gv~%_B@VYCxx{9)
zWwtEdIIU`f{`~-9T_H5<Q~R?DH>#et1<5^owQzSM>MZQ4wRtPQkj7xcr{v)nKAn1r
zdBgQBF--0TWjUjasaINCU{&Z}sxMH%G%PjeSu9I5aRdX^N!J0>-s^!nNt;@|DK(|p
zsHgL?@OBS?N_07}qW~+d^DAgSC<Pp!{oAZ~mwLl)^ts22sQO-qnAT+koBJw&t|Lj*
zwk&Q<4xseeJOwbWCeNcl5g_hKVO%=0umD{A3-Bbs*8xhLU>qn1KP}r&WoGGMV>XjZ
zX>{SRDZ|CnqDN)e&RslPU20Zq`_kZ0-mJ20k(pZ7w{hP3rpuZoNs0E^`i5wIbG=uZ
zZZuj~jdtl;PJmU>9l+G^<CNWT4Of~Q<1H3rzXz~7Te=_U(xLAJReQ>Wo<#2{lf*?l
zfzHVBWO|u{o&|}kqx9#|=AdHcz#F9}xHv=hS7zqpvNMSTNwp^3)utR=_-ENdWqzq!
zID=KovpQ@SnVAPS13g1jLsY^j7dn;9SJQyfnhNGud&7PBbj1NVs$@ro^iz^1SBRzg
z<KU#}%ei)3V48}8ksOv7TFNpFtgmM^=5>0C>`@J|prFix#RFxQAY%1E0Urp#)T`_c
znQL#7?v~gTjXNJ^CMn`f>Ps|U0Z?DiXP-q|<Lz^X-U0Lsb^SHa06-=FoH<YH`)h4J
zI@#u<B4wP#@V7bNUZQQTQPbO8!$m)3{?VeTuDKCX(trb&m*(50AyLP39tf+XFvl^c
zo4-XFcz#92?gFZg_yRBuv@Zg6>$D=?CKV?;)G#clqAnrVSyjY{hg46jl(<{!aUNE2
ztXNFu27F%leT)8`S9XSyxg>w0{%RRfr4ii+Hr;97v8AHkQ8=3(-&eii#w<*@0{=!^
zqacgIY4*ekJ}<Vl94so_lCcF=xFh4hH3mt#J!<`-e1>Higpz6iKeVhcn0<HNsk*2H
zbZYemrsskLs4nLmFkQ~Of$DjUd%o)ple*vgK9t8z+16%CQ80sDXSa#8z(;O94e60v
zb*P0k=}hf!fpayr{})i*vgqVUK9v|3vd8A-S3<+h=W93$39S99A=~t&W?!lyi+~3&
z8KO*80lA)@$9%PeTe=C<vjSBfwYVUidKcG2{#LCwg87Th#`XcKA(*aYsG{xHlE2^F
zpGdDOqgRb%TYW@@)wpgmjtr+MfH|oG%(x*4RO4x!2|NXg?q}nI`HKNAk%NYum+Ny=
z)kZ_E<@ocE?jh1&S(FRP;*_0<(7EA5W~09_o8P!0sw~VN=@kJ0R}TQEuM_h%)y)^g
z<2vLwlJgC)N949n^_d)rn~h3s3B1k^stbYYl)xww=SaW46L}*j*JGXi4FH1xTQOO*
zK&GI|cqZrEMs@*OO|)XB^|fEhN3yS3JydNTQ91)dZPFR@b@mhV36{`LKwQ$p6>&&$
zzXLrQ1jaGS!H<FjXZW3F1o-{r`4ZR-z%BP?PC1UY4j3#5?hq%^(~A!VF^Ov|2+(#&
zem@E9xlWXwqyR(_NI^TZf;%h3mTjM}2J!AThViJaGkM{i$qR4AF(RVe(hSskJI#^W
z15_*C3{dOTBW{0dr<PNVDEdIp(?kz~RZH(7pmO2Q>TU8t^;Q#}vuoU9a7#5q2V9!2
zGE-eybMGqsB$%E9c!Ku74^%lVtJFkWUgWu7_@H__3}K!cM&*xl+m66W>eo;%HB{DI
zL#?!@8JE1DXpLlDqKbN=r^@*({zAlUTx1WKVajEOsT8RC02c&?`lIcEkU-$5S)^@r
zmLrS0rR`BZ{g7FttY#7EYs@0hJ>RCHxJE4a`vw3Jp8hDnLjVtSs;9@=#e?%Wb)c)v
zH78icMnFFX@CfE`^j`uDoc;;`TweSMlFtbm6;7_KYwIjqt$0{ng7G>BFp7H`*w;Fd
zPk{1tBm?blV0I0mTsf^wDuYGyVeovD>;hVfCOXH_8I86nxDfJMWWHlH8RF7Bim?*_
z*ARU8FtB|a01@S1pz|@g2E?#dLiTEH9O^hP&oP{LxSbAJF9JZLxCqjaYqBEP5Mq3-
z%<u4c_vT;A5feT3mOFsvGWquvpt@l(_X8-{jQlL~<N>tx_{c{QMHy{c?~Z~l<!pCa
zRi))C06zwpZ7FW(nYRh^oXoNd^cp}tcZ$_6|7D@LQ&gRY0WQFU=+sx2alt$b*3VlC
z7P>XjDD@q*4+F^F>iqpC5PtJ)4kHfSR<w@-FeP6F_87q9U~13USO4#fWvG1#B08sO
z$D<CNMGar$Na|@v9V0(uG2AgjIs7bS{O=4s8_59YZ)tG1pqgVgTYHB7p6p=EBS~&D
zXg^DcJ=5=KKVWF`>;&yNpS}G{gJ|p_w-sz=F2P%%yd)sakmu1xLb=f_L++PG{Pn_Y
zb>IGav%YYo<4K|Bn6$iqQFVD83w6md`OwD=2$$UGO&`wfk%{r{0_=-2sYGrF^?wH{
zIWmJ!W#r>yI#Bx3Y<q+ZwD-87C%|y7D93Mk9nt_r?#fqBfINjP@A2}6gXV2=49BN)
z?*hCBKvkmW%|Z`)J>yK?SajT;sZJy1oLq0DuSYiBNtq53{s}p61N;?$emf<PS@P(L
zw)5}O{=b<Q%9;Dhxisc%d~aiPQD-K$x=(MjWk`)Yk91Fm(zzT;rjn?UEPyOp*lFwC
zBEGtt;)|}w7U18@6>%qfSj1>nT8J>7XY-d?Jff$<(+t$Wm3ZzvNir;OWlnJ%wlLR?
z&XoWw@C_m!rswADWiDV-2rJ|<t(Hu+J^+UmAn{~GAD5)S9iHOLxZc4SVZ)hkb?0WP
zt%*%KCQ>|OEP5J7O_7%oe8IF-pFfnyiP=1IIv$=EO+5+YEEztLJ=0ruK_0j7a5=Ej
zV3t5;svFIcVKkr14`p*{aLZ8LL3bc}+@)ww080R(10vfzRQV{-5@r!jA}-N6C<gf*
zivfvAtDTHG-ZC}nMk$2>Wts*Q@aUKr$>VtWl7PVoD<_GC4YJ^pNBklJH3hR`&HO|@
zfuD%g#4;}f=pz@^gs6bW(13%T7CuS|Be}6*M5Tc1Isqz`7IG+SK^SS@tJLL)Vt(<>
z3Bnj>MUIE<`5KUvTFlVC8}u;@+`;jT;t}%Wn4qj-s35qz8X#qkgj4%2khViaoRVpc
zGtKxIyuxPMV)jA_w+dqNI3X5xfS^@H4X@T3X(8>;gDvdB$X%w^Ub9)9PEy+<=v|CH
z;CSc|^nMKMb)|}fX^q7biN2kJwin=b>W`Coy0n}XFJS3dV0V(~oG}UJic-qt!9{{9
zH-=+h2|`5jrvgpw>8#V0V~y}w$<v^-=c7PgeQ!bPX*&<TFq5AU!W<`Hn9PBb&KR-S
zNYJ^<R&1JD(mPyC?gXs4!N$YQE>H++r&3Vu!@Z#BOYT{;rx`tEqI6Swv4<Cy0~B)-
z?-=qM5E*qqfbNSL7m}&^0}cN^4v*;u0Zv`vr!+9pp|u!Og^yTUFx~$;*Jdpwyr^3t
zk&@>z>>>bO6vCxyf^_&bO1um>PK$vzy>O+VyuSsU3tSikpiAXj-3q$0f+rY`TJjMF
zbDwKIqE3a(@^p~6fLM4UDpuTJT^MaI7#P1DVB8jZOxj+nwZ%SGz`r;I)|&v73D`Km
zQv!IO(#0re`8l8ECz$raDH<V`Gf_?B3P%yAnV6fbg^x@V^wwPz3ZU7CgHYH)ekLBn
zQiXz|C)YQ~BtQd7N@$vWEvmwUT7y-;X$&Z%a|@@Q1!`fALLOd-atZDI=F$Z1U1rI&
zv{l^A<`Wb50?6%I^Ii0P2b3sl4p`P4fFvy#vNcIUQF1p>q>Ans%ohz95N^m0*~ido
zd5oJqC@+`wTE|279_eL_`E!um&7V``zp`M7V7&Z;zoy8(P_`fQ1i8ZEf~faAx0y!#
z5FL6i{gI)#eukfs;U_?ULG-6U&-7+O==lG@z43Pcn6!0!r&s*LXouV@dH~^0&r^sF
z9j5%p!5SUEqM<V&B><xU9KTuL9O1;YJIl$*1g9+*elrNj0O*k3dJ<uzZlw1(94?f{
z#;h3RdHn~N>$XxD&Ozx`o*Skc4i{hooMnK7a;b6@SZ`(Y@JC=WS*GysOyLfPyh!0q
zGA_KCj;3>>^U_~bRj|B8{lJjwiy=@l)eo&VnK9fbOfz0d^6wL07QTY~QsvggitEB?
cek0n_lx-AL{47p?<B&I<AFs_$;5Ul@1qmo+9RL6T

literal 0
HcmV?d00001

diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean
index fcb0cb370..ba1a29927 100644
--- a/src/builtin/optional.lean
+++ b/src/builtin/optional.lean
@@ -20,25 +20,25 @@ theorem some_pred {A : (Type U)} (a : A) : optional_pred A (λ x, x = a)
 theorem none_pred (A : (Type U)) : optional_pred A (λ x, false)
 := or_introl (take x, not_false_trivial) (exists_unique (λ x, false))
 
-theorem optional_inhabited (A : (Type U)) : inhabited (optional A)
+theorem inhab (A : (Type U)) : inhabited (optional A)
 := subtype_inhabited (exists_intro (λ x, false) (none_pred A))
 
 definition none {A : (Type U)} : optional A
-:= abst (λ x, false) (optional_inhabited A)
+:= abst (λ x, false) (inhab A)
 
 definition some {A : (Type U)} (a : A) : optional A
-:= abst (λ x, x = a) (optional_inhabited A)
+:= abst (λ x, x = a) (inhab A)
 
 definition is_some {A : (Type U)} (n : optional A) := ∃ x : A, some x = n
 
 theorem injectivity {A : (Type U)} {a a' : A} : some a = some a' → a = a'
 := assume Heq,
-     let eq_reps : (λ x, x = a) = (λ x, x = a') := abst_inj (optional_inhabited A) (some_pred a) (some_pred a') Heq
+     let eq_reps : (λ x, x = a) = (λ x, x = a') := abst_inj (inhab A) (some_pred a) (some_pred a') Heq
      in  (congr1 a eq_reps) ◂ (refl a)
 
 theorem distinct {A : (Type U)} (a : A) : some a ≠ none
 := assume N : some a = none,
-     let eq_reps : (λ x, x = a) = (λ x, false) := abst_inj (optional_inhabited A) (some_pred a) (none_pred A) N
+     let eq_reps : (λ x, x = a) = (λ x, false) := abst_inj (inhab A) (some_pred a) (none_pred A) N
      in (congr1 a eq_reps) ◂ (refl a)
 
 definition value {A : (Type U)} (n : optional A) (H : is_some n) : A
@@ -69,13 +69,13 @@ theorem dichotomy {A : (Type U)} (n : optional A) : n = none ∨ ∃ a, n = some
 := let pred : optional_pred A (rep n) :=  P_rep n
    in or_elim pred
         (λ Hl, let rep_n_eq     : rep n    = λ x, false    := false_pred Hl,
-                   rep_none_eq  : rep none = λ x, false    := rep_abst (optional_inhabited A) (λ x, false) (none_pred A)
+                   rep_none_eq  : rep none = λ x, false    := rep_abst (inhab A) (λ x, false) (none_pred A)
                in  or_introl (rep_inj (trans rep_n_eq (symm rep_none_eq)))
                              (∃ a, n = some a))
         (λ Hr : ∃ x, rep n x ∧ ∀ y, y ≠ x → ¬ rep n y,
            obtain (w : A) (Hw : rep n w ∧ ∀ y, y ≠ w → ¬ rep n y), from Hr,
               let rep_n_eq    : rep n        = λ x, x = w   := singleton_pred Hw,
-                  rep_some_eq : rep (some w) = λ x, x = w   := rep_abst (optional_inhabited A) (λ x, x = w) (some_pred w),
+                  rep_some_eq : rep (some w) = λ x, x = w   := rep_abst (inhab A) (λ x, x = w) (some_pred w),
                   n_eq_some   : n = some w                  := rep_inj (trans rep_n_eq (symm rep_some_eq))
               in or_intror (n = none)
                            (exists_intro w n_eq_some))
@@ -96,5 +96,5 @@ end
 
 set_opaque optional       true
 set_opaque optional_pred  true
-definition optional_inhabited := optional::optional_inhabited
+definition optional_inhabited := optional::inhab
 add_rewrite optional::is_some_some optional::not_is_some_none optional::distinct optional::value_some
diff --git a/src/builtin/sum.lean b/src/builtin/sum.lean
new file mode 100644
index 000000000..46aa6f63e
--- /dev/null
+++ b/src/builtin/sum.lean
@@ -0,0 +1,122 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import macros
+import subtype
+import optional
+using subtype
+using optional
+-- We are encoding the (sum A B) as a subtype of (optional A) ⨯ (optional B), where
+--    (proj1 n = none) ≠ (proj2 n = none)
+definition sum_pred (A B : (Type U)) := λ p : (optional A) ⨯ (optional B), (proj1 p = none) ≠ (proj2 p = none)
+definition sum (A B : (Type U)) := subtype ((optional A) ⨯ (optional B)) (sum_pred A B)
+
+namespace sum
+-- TODO: move pair, pair_inj1 and pair_inj2 to separate file
+definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b
+theorem    pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b
+:= subst (refl (proj1 a)) H
+theorem    pair_inj2 {A B : (Type U)} {a b : A ⨯ B} (H : a = b) : proj2 a = proj2 b
+:= subst (refl (proj2 a)) H
+theorem    pairext_proj {A B : (Type U)} {p : A ⨯ B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b)
+:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2)
+
+theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
+:= not_intro
+     (λ N : (some a = none) = (none = (optional::@none B)),
+        let eq  :   some a = none := (symm N) ◂ (refl (optional::@none B))
+        in absurd eq (distinct a))
+
+theorem inr_pred (A : (Type U)) {B : (Type U)} (b : B) : sum_pred A B (pair none (some b))
+:= not_intro
+     (λ N : (none = (optional::@none A)) = (some b = none),
+        let eq  :   some b = none := N ◂ (refl (optional::@none A))
+        in absurd eq (distinct b))
+
+theorem inhabl {A : (Type U)} (H : inhabited A) (B : (Type U)) : inhabited (sum A B)
+:= inhabited_elim H (λ w : A,
+      subtype_inhabited (exists_intro (pair (some w) none) (inl_pred w B)))
+
+theorem inhabr (A : (Type U)) {B : (Type U)} (H : inhabited B) : inhabited (sum A B)
+:= inhabited_elim H (λ w : B,
+      subtype_inhabited (exists_intro (pair none (some w)) (inr_pred A w)))
+
+definition inl {A : (Type U)} (a : A) (B : (Type U)) : sum A B
+:= abst (pair (some a) none) (inhabl (inhabited_intro a) B)
+
+definition inr (A : (Type U)) {B : (Type U)} (b : B) : sum A B
+:= abst (pair none (some b)) (inhabr A (inhabited_intro b))
+
+theorem inl_inj {A : (Type U)} (a1 a2 : A) (B : (Type U)) : inl a1 B = inl a2 B → a1 = a2
+:= assume Heq : inl a1 B = inl a2 B,
+     let eq1    : inl a1 B = abst (pair (some a1) none) (inhabl (inhabited_intro a1) B) := refl (inl a1 B),
+         eq2    : inl a2 B = abst (pair (some a2) none) (inhabl (inhabited_intro a1) B)
+                := subst (refl (inl a2 B)) (proof_irrel (inhabl (inhabited_intro a2) B) (inhabl (inhabited_intro a1) B)),
+         rep_eq : (pair (some a1) none) = (pair (some a2) none)
+                := abst_inj (inhabl (inhabited_intro a1) B) (inl_pred a1 B) (inl_pred a2 B) (trans (trans (symm eq1) Heq) eq2)
+     in optional::injectivity
+            (calc some a1 = proj1 (pair (some a1) (optional::@none B))  : refl (some a1)
+                      ... = proj1 (pair (some a2) (optional::@none B))  : pair_inj1 rep_eq
+                      ... = some a2                                     : refl (some a2))
+
+theorem inr_inj (A : (Type U)) {B : (Type U)} (b1 b2 : B) : inr A b1 = inr A b2 → b1 = b2
+:= assume Heq : inr A b1   = inr A b2,
+     let eq1    : inr A b1 = abst (pair none (some b1)) (inhabr A (inhabited_intro b1)) := refl (inr A b1),
+         eq2    : inr A b2 = abst (pair none (some b2)) (inhabr A (inhabited_intro b1))
+                := subst (refl (inr A b2)) (proof_irrel (inhabr A (inhabited_intro b2)) (inhabr A (inhabited_intro b1))),
+         rep_eq : (pair none (some b1)) = (pair none (some b2))
+                := abst_inj (inhabr A (inhabited_intro b1)) (inr_pred A b1) (inr_pred A b2) (trans (trans (symm eq1) Heq) eq2)
+     in optional::injectivity
+            (calc some b1 = proj2 (pair (optional::@none A) (some b1))  : refl (some b1)
+                      ... = proj2 (pair (optional::@none A) (some b2))  : pair_inj2 rep_eq
+                      ... = some b2                                     : refl (some b2))
+
+theorem distinct {A B : (Type U)} (a : A) (b : B) : inl a B ≠ inr A b
+:= assume N : inl a B = inr A b,
+     let eq1    : inl a B = abst (pair (some a) none) (inhabl (inhabited_intro a) B) := refl (inl a B),
+         eq2    : inr A b = abst (pair none (some b)) (inhabl (inhabited_intro a) B)
+                := subst (refl (inr A b)) (proof_irrel (inhabr A (inhabited_intro b)) (inhabl (inhabited_intro a) B)),
+         rep_eq : (pair (some a) none) = (pair none (some b))
+                := abst_inj (inhabl (inhabited_intro a) B) (inl_pred a B) (inr_pred A b) (trans (trans (symm eq1) N) eq2)
+     in absurd (pair_inj1 rep_eq) (optional::distinct a)
+
+theorem dichotomy {A B : (Type U)} (n : sum A B) : (∃ a, n = inl a B) ∨ (∃ b, n = inr A b)
+:= let pred : (proj1 (rep n) = none) ≠ (proj2 (rep n) = none) := P_rep n
+   in or_elim (em (proj1 (rep n) = none))
+         (λ Heq,  let neq_none : ¬ proj2 (rep n) = (optional::@none B) := (symm (not_iff_elim (ne_symm pred))) ◂ Heq,
+                      ex_some  : ∃ b, proj2 (rep n) = some b          := resolve1 (optional::dichotomy (proj2 (rep n))) neq_none
+                  in obtain (b : B) (Hb : proj2 (rep n) = some b), from ex_some,
+                     or_intror (∃ a, n = inl a B)
+                               (let rep_eq   : rep n         = pair none (some b)
+                                             := pairext_proj Heq Hb,
+                                    rep_inr  : rep (inr A b) = pair none (some b)
+                                             := rep_abst (inhabr A (inhabited_intro b)) (pair none (some b)) (inr_pred A b),
+                                    n_eq_inr : n = inr A b
+                                             := rep_inj (trans rep_eq (symm rep_inr))
+                                in exists_intro b n_eq_inr))
+         (λ Hne, let eq_none : proj2 (rep n) = (optional::@none B) := (not_iff_elim pred) ◂ Hne,
+                     ex_some : ∃ a, proj1 (rep n) = some a := resolve1 (optional::dichotomy (proj1 (rep n))) Hne
+                 in obtain (a : A) (Ha : proj1 (rep n) = some a), from ex_some,
+                    or_introl (let rep_eq   : rep n  = pair (some a) none
+                                            := pairext_proj Ha eq_none,
+                                   rep_inl  : rep (inl a B) = pair (some a) none
+                                            := rep_abst (inhabl (inhabited_intro a) B) (pair (some a) none) (inl_pred a B),
+                                   n_eq_inl : n = inl a B
+                                            := rep_inj (trans rep_eq (symm rep_inl))
+                               in exists_intro a n_eq_inl)
+                              (∃ b, n = inr A b))
+
+theorem induction {A B : (Type U)} {P : sum A B → Bool} (H1 : ∀ a, P (inl a B)) (H2 : ∀ b, P (inr A b)) : ∀ n, P n
+:= take n, or_elim (sum::dichotomy n)
+    (λ Hex : ∃ a, n = inl a B,
+        obtain (a : A) (Ha : n = inl a B), from Hex,
+          subst (H1 a) (symm Ha))
+    (λ Hex : ∃ b, n = inr A b,
+        obtain (b : B) (Hb : n = inr A b), from Hex,
+           subst (H2 b) (symm Hb))
+
+set_opaque inl true
+set_opaque inr true
+end
+set_opaque sum_pred true
+set_opaque sum      true
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index ae2bfc763..7db68e73f 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1522,8 +1522,6 @@ class elaborator::imp {
             }
         }
 
-        if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; }
-
         if (!eq) {
             // Try to assign convertability constraints.
             if (is_metavar(a) && !is_assigned(a) && !has_local_context(a)) {
@@ -1549,6 +1547,8 @@ class elaborator::imp {
             }
         }
 
+        if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; }
+
         if (process_simple_ho_match(ctx, a, b, true, c) ||
             process_simple_ho_match(ctx, b, a, false, c))
             return true;