From 9a7ec6adbfd12e5305800a033d1b471afe316abd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 02:13:35 +0000 Subject: [PATCH] ... --- .../matita/nlibrary/algebra/magmas.ma | 21 +++++++++++++++++ helm/software/matita/nlibrary/depends | 4 +++- helm/software/matita/nlibrary/depends.dot | 6 ++++- helm/software/matita/nlibrary/depends.png | Bin 16838 -> 29280 bytes .../matita/nlibrary/logic/equality.ma | 22 ++++++++++++++++++ helm/software/matita/nlibrary/sets/sets.ma | 4 +--- 6 files changed, 52 insertions(+), 5 deletions(-) create mode 100644 helm/software/matita/nlibrary/algebra/magmas.ma create mode 100644 helm/software/matita/nlibrary/logic/equality.ma diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma new file mode 100644 index 000000000..de8e3ba22 --- /dev/null +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "sets/sets.ma". + +nrecord magma (A: Type) : Type ≝ + { carr: Ω \sup A(*; + op: A → A → A; + op_closed: ∀x,y. x ∈ carr → y ∈ carr → op x y ∈ carr*) + }. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 857215f68..1b7a60cdb 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,3 +1,5 @@ -sets/sets.ma logic/connectives.ma +sets/sets.ma logic/equality.ma +logic/equality.ma logic/connectives.ma logic/connectives.ma logic/pts.ma +algebra/magmas.ma sets/sets.ma logic/pts.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index 710415825..eb6855410 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,8 +1,12 @@ digraph g { "sets/sets.ma" []; - "sets/sets.ma" -> "logic/connectives.ma" []; + "sets/sets.ma" -> "logic/equality.ma" []; + "logic/equality.ma" []; + "logic/equality.ma" -> "logic/connectives.ma" []; "logic/connectives.ma" []; "logic/connectives.ma" -> "logic/pts.ma" []; + "algebra/magmas.ma" []; + "algebra/magmas.ma" -> "sets/sets.ma" []; "logic/pts.ma" []; } \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index 631218af159fc61cadef10e8bce1304422377a7d..31bab15390047a8bf2cb44dd9a8720a13ea21c2a 100644 GIT binary patch literal 29280 zcmdS>cRZK-9|w$ojF8M0*(6C>4av$1AtXscM%jDMC?i6Y3YCx~$qLyas}dR6n<5z{ zBPra^>zwnw??3MQ@%#P$yno-Xb56(M`ds7ve!ZUSbw%iCsnXN3(UM3c`jcwPx+D^r z82&1!p~82RquzbRKd8(#RFz2^#Q#$&GvY`j9@0r=1wHSFGlKyJdLHY?*C*)?Rnr}! zE2f~Ui#|HwtyJ>U2fF*-%O##q zbhP8qH@p#k^w|@-1U^^MqZEg#2gGxSxz{ER)RM08Sy7q9OiQsidw)EZ>o)Ol(kJG<*Ef_K$PL5A63ngYQw zF^uFC6n_eh?5)R13*xN!C`s0~w&Wy(13L?giXuv_&z;KDd-L%lBZ-NFgKi`vWnp1K$<&mGoSb~* z`*+4@mE9p$&dy?g*Va;X1evyPr^LBD(-WfHw24T_av3_4R8mdV2b2xw)!m&cta*9yxln{O{Zhv&WuWYBiqHR7mKe14jQY*AKUZ=-z1Uls&6VaV#w5^jaH$kt}OoiP+NPo z{gADrV_5Cz*ZGYWG0$%US#EM&mIa&5><=cI7W9rdOSTRS;BtnZ)SF*zv)+E~HEz9w zgM-+EX5wb04sRU2&y!>wDl!XqLS^z^nrPD@Mem||jQk1Q#XlrvZ|?V(DjH?IlZ z!lI+E-!-daY%E-OR&e_p=0gGkRQR<)N9W2U6Y+^pU0q?sd3ANsQa41hh(3P$lxoM0 z9f~nSKHm=DQSaCh8WKWT*U-QxCpUDNwT0~H6N(pUX%v?)Ul!cAuO{)3m5#11d8J8A zd%LdQ*|RmJU)iD?E(fcrsWDxNiH_bO!f;3;;r{*mIwmF}9C{y_ z6sJlISM-x7{QP_N@E$w1>*UFk;gON-?V>7l5u^fx11qD~xpnmPLdM3-<5OHsyl&u1 zb#=FH-L~ykLc-Urx-F4iQ9f}`p9;jw?-v#hHOW;yd2+LmkPzvwyKKuY`-q4LH7%`% z5|?o?#{tQe)zupnl;=K9lfQWNYUf_dq?^m*y6laUZRWi58J*;`!J>51m#E_^N_WARrC+X>Ce^=%c#LUQZs@8q2iwyHM zzO%$I-i>3%q>aM z*T)-U#y@4A5j=39E@InW=g~KtNb;91@wd0P$3A*=^TP+tOO}>={QSzFpZiUSlTA2F zIs`u!Tq%6J_b0&CY#rs3@aqfl5kBtMRZq!RB^6j`x@7}$;vN9esKb4Wpcl46XWW zo3_N>y&H z{%SUM_W53`0z}j#4ka*}fgL^|*%Bxor{(okRSH>bm^8)^O zveHp~ND!y+8uHnDPxRuIQ*#*{c_cSUj-E=tqeH&a!k4V9YP-8xn(hhL&K3{f{Jk)# zBofb9XU}S3Qf*nlD=p2=9k9skIXAHRL37xqEjvfLtJaUaeEE`U=3v`dY6Cw%X$gnE zkaHIUc1*S;)&BjxkncHbc)+;q&ah!EtI~xF?D*A)z_sa%Z{NMEd3HMO$B$aZ@gcwO zvr7e|t06hD_2#MZCcY7TyLX?=)N5B_lvVbvTvy*a*+yzT`$8xt>D;-{&``>tv9U4b z#N+I%i@vgJ6Gy9fLlqUIl5Uz@`F;6iul+fh%Kd$3mS=jEu>7Cs2!3r-wVT^%H%0F{6!v<3b$b7Ottu^L2MKnrz`riU zQ^bBIws4+VEtRsevXSx8Sf7x9Kg(n!%MS^>u6yjCMTUo0ZxO8sircGg{^{B21Zgjk z^_9lsW&Sc}lNXOnq47;k9^W{YsVC(7z4BL%pm61mFa^dBqs}@82CQT$*d_|e$JvL5 z0)83mX6m_joH}~?!i5XT+}#!i;&gFN9m~3XXNEco2aPT2fc<*2@4C$QngZZ`^z7){J;~f zqV)Rp>%*>})qH328{e9Wxl8BXySH=oi)i4f+(ap5(eRuKnygYW@q5susU*EF+m1y>(CT(SNAALDz`sQB$nd9nTPH&V+DDo|M z{Fo0y8)vpflXIyA|<{mDrY zhjPa!RU2#HHpYv7XlGtTW5WjCc};NT(YojxtjQ}1(QV8F<*!dv`=ipp(G z0k>n1fB*SYUN~E}fNsZ3djIa7i%on|(rlN+?%ly8T;1yn^ys^kLFkFI61h1Un}|C@ zx^w&XSl9CLjo%;7idvvGkfn5FXnU2kPV(Ja z{Cy{7S`y%pe8e+9zo@7)J6kuCpM<5WBqt}we^>pa(A}~R7e(UBo3k=(yoPj=9I(-H zZFfaRMs6nA6d4vzN%r^6E?pqm)_+gNJNWgccTF!*25CK%B<|NWaf=2fk}oR8$=vQUD2dF>=d-)W7{w+t8^46* zEPT@rGM+v7da3IIWsv?0gHeg3M-y$`^J|&o>J;{3w!2rST;CTDU(vwj$z&Uq-agDm zPnMFd5nt9kt!~Hm%&@XI-=dL*bob63qgM{e_k6ovoG-L&zMqxdWbyWkD>;unrPi@y z#{&9JKg^Iaz8LUrZhqTdEq;>ww@;aJofH24fm*z|p1YDn4^}Mq*~xafrH}tPqZ-&X zZQ9+H`1g=b=L(`wUiXl;Z{6BHyWm?SZ4%h!5!gL#+SS$X<~1Dfi{9WA z#p$f0u96&!XpMKD=-MPZrSg26^y5A1G^FWT`j99UXV0Ep6KOxwGwbQQI+d|cKp^b1 z>#=B7@oQbV7qxdrrhimjy?uMDVWBnizPswQbaYQHuK$c*9FIA^l|;+P==H$L(NP5T z@t^uH5+A3Snt~P4PQfTM@{=~*&7`@x*&Qw73<%REO3K#ubd4!skofGZs-_a31xs?@ z*EijWGw=2wo_g24_;}S{18$6a`1xZs1=50oNcSaO_$vSYY!YD^$vqpiMrBdzbR|2S50^?y(IeAHrnm<{zjxW7`hHgUn-W#U7kd3?K-*PsUrSqjTV|I;(N zzMrF~?;1ZsU#Dl6h*eL2d~3IA`)KX;KeEyLZ_E<)>gT(?CsTEF{QYGd21;CdHuVzc zTYZ({lEi~|redx4gf9pR3Wf*GiH7+-2O}VtSG~!>T)v%;O=|k?(g*YWR(7Wfh5Y<{ zbb9Nx)ulDx4GXJto!<|Lie`9Bciqa(6+Lm{MBBxU)o$L6HYqJxW5$!(+T5OIay4h?-P9w_$i2;dbK0CfWJAZQFP5R3R49Li5p%R}TF- zl4mPx;xAq~xiHb}=I7=)`RmBb_3cP`Jh88w!ay|Vu2d%o32E}+D;ygVi{GO~nYZUV$7Uv9d` zD;1;kI9)nsTUUdud_0Ypb}=BZ|>WkfUUbk)D)VskAPLg-C3 zef^yi%@3}#JC>NWO7jJCnHqO~`egd?ku33fE>Bzp2OmW6~lE3-%2hYA0GmK|NQw=$H<5-Q}4!|JKHsJ{=@|XI56$nwa+&DF}1-t z><&ryuS{shp@mK$@9OD_wzfhIG2Ahmw+ZkF3)2HvgsP`+Ex*)IaqrzF#nY#mQP{5% z3(*;HEmPDmH4P0VUtg()s9odpRb9P@#>EGKGL+7pI`ZpI&>Qv?I&QS8X8+jJkVUyRAW>W70JiO#|Oi*)}OmI z1#F;bONb+fIJm8@OgFShY`HHrtW{6@clg~b?mRQ=nA-!|w zlybZAl~!2z>B~DOYip)HY}QiBKA`je$q-UfY!C?uamVFkk4|S>+tt24Lp^={$7N+~ zz!}e;J#+5W&jRFH2H+Iwe|{+C_U+qX`+LT2(>*fVW?BjAE28?cgUa(w+zND!U8CylE%|GLH7L1-?%VXV3-lG7VcOHDDm0nz->X9u zNPYgC*2BZ&>({SLTr6yCH+p&u;$y%0PmI{Ge5$V|>!OBshT=}h8xpTtRNoP2s;5_N zeYi|UD_xgYMux*Md#9P1*_)LADK1dEqE&)ZQc`$3E4gnFnwc0YG@~ep0iU|Nw~XQh z_Wm`#crgZtGAeW5oSmI5(gA_$U$Nv)(^Z{}4uy;kY(6$zgFk78f+3IWQ(xZ=6zuru zl7+AUT!mR}4#b}RJhEzVJBV6}DIT0s)Jf3s)YGq3RULJE{}0k#TASeC;ayr(!DNt;9LHbiXZ0^qkdrg*+!^-v?OPK@JzQbylsgR# z4U?HL-6;-JKG#QvV4h}Q%W4-34;2*^)m%EbBoz>$%omb`kG~ciOeVj=P67|-xuphC zDAezpp3n{~W$c^7Y|%}J0|Em42Fd)kXj#QBJ^`u|<^iwA_JGC~^5saPW?rwovm^)9 zEvg@9L`y3xIh85F-j|m>6PhjY!A6eT&Oz1_y8EU^0Si)6vS&7>ZOKYUhw06mHznN% z_!z`Qtq!w6t~A5nA>Bc@Y;V5?VHCg5JM&Qb&M;+E8++l&JW)EAsdO zLdn$4OwrF8{r>%9_pJ&JYSwZ~{cOWcq!m!&6FDLDXCDPT5VnX~x<(NtK2aoD4GJFl z|MEXVcQ$9KsTf|K?Vq1`;KX3YF5l@| zS^-`9i!1)@`GeM6iR)K&Pf*+R62zOiqEk?lPy?tk`6NEMFh_(+ z-z}aaNAA`}(hK7AQ-GZ*xVgED=fMsP3M`{(cI2lv3{Y55i171Mo8I2 zA+mSY6ZI~oqJjge>VLZMX=CGP6fZ)l2FwtMd-uhKHuP~LiH3neMP5Eg!+GWRZv`Bm zhld2Lf#Y9O=DP}i!7$r1OCwufNg!^tNwkWRbilBX#!78Vhx+q#lx7k>R}B$^Q(AEEvU3DFv6cR5fq z(9?4ko;mcOnTk~Ty2g(OJm&D>!!(u6Wo1%CpUBD4Vm)`^LL{`fH}(<~D^ojkA*=(w z)-^WnmXqUxj*5mzh`=a*)ajm{mnExZlzn`TX(dU80tn!Ycni_5Dd8O`|J!Cmhm?$r z9=1LRkBZvvv$;a!)G2xqqmrPXKV6MVoNK;RJI@UqD}42eob;x)HdIVQU0qRKot98k zaoxA#gUC2cgIgSn(@IKMA)&o-{=4FGSVDrFWNu*r5jq@OBx=_om6f%!>6~q)KS$H? z3;`0}TvbMQ24Dd5CS55zd+ANcW&n|GVR!D_aU7<8pTo(JXEy`H4iUE&8sx3``0Kz= zHTDv4RLuWHE!#XpT*e!Cd3fY!Zl4#07Is=skDtSv*!oaaMvtA+(5Qvx;ap39l;_Z) zZGg?@@iI?bg6Q*rCj8fyx(Qszz#&PhG+~5jO~4^wzyxrVE6WARyyD`wV!D)+Cry^x z(p2Z6c8vn2K?Eo6FEE;8$tcx_`$x9S&(E93OFwZAG6vE6M-znvso?1;aU(Jk3UO>= zVg#WkC(Cih37i^x)G5}1CR%%)alHKdYb6sCE~pOS5Xt!W?zO17wkhGL6PIPn!*|8L zMtd0Y_Upiw!M+=ZyurBqeV7sACP^J@yhaJ^2(5BplvA zP^X9A1gt*#s^77eSn{*$0uqH#y@!B37P_skEyFxJ9G2gr*wx}d~3+M zqQ8B!tyo*`_lB4ZZ88#ig!yb=QNr;+xxat^)``T>o9&F;bTMFQ2h?2InSs)6fFmW~ zia)Y0uF*o~GmoEik*t>5CoEi#3yap4`%MW=vE(V+?oW?iiUjqn*)^VdVL4{TLkQYJk&O^=I%q z{I?yeILoWh zU#UsB{D!mIS$iqYPCFA??#yr%x3=uk_A9^2hetQosx~H<10E_3=B@GT zX1@e0z$jEEq+lpC5ym&zA2h45OW3Et=7FBdANLM~>ISR`Ex+X%7n?tLeyylOYH4k; zAnuS!Z*%$0h#zF7Q)DN}GOQ(D1REpcNz$5}FIuiUCj9@i0_~jG0Ch&SYNcLOP)h3l zrGvX*2Dajw1f`|_yj)mx%u?S~zY4%=+q!NPI|I6(I2+uf8wpKLvf$6+PT9E?T-Y=>R|=_Pj1F$24vcVO?S z`|iDLbw40owEwdbEp+I9ld>{1c}a`V&Tbg17ylzq3mfDGUHQ{L+>SD+EhH@LVH0=j zmI6ue`0?S{`Tt46!co)0+gFJ*diz$5Ts}iPd6~Fp50@cfg}8uRRo(Re{NNyEKRW7a)hC&E{*APK5afO)dErM|Z~gW65pj7n+FSsjPLSKK#Eh$ML#p-7*;RMF*hnEI-#It`d z^qAI&)o3Y~+r^=HHIFG|OB$sDA{#Oj= zZtLWrh+EbL-6C9FnSR0H$)HY+%4I2}Eqh;Zw%x(LY4 zNm88|jnaPf0Re4~r~f`=8NKK?dn6{e=;%3iQz(rjnwl?n;^M|}gwuwHXQ*aq zQWW&hE-oZ*JcKnjx;y|DwM1v6l%Agcq|MqI?1O9R^Td}gZL+@xlz_pA`oqH$B%t+B z4OY&}3q2DP6YV#4>?djj=;yxev~197WPemsh~%zfe;F1#a>8QYoT1Q?H0!$1U*Y2x z)14rbt)F4H!xYZXqbsX6F!y;OlY+mbEKPUE)tk?k5Du$5x?G$}S}MBi=^0n5=t&uh zU{lyQpQooa?7DOIWOWL89^;zIDWBsbE#mgyFs7Z}UC^ruMj-${qp#d6x91Dpb2AtE z4>s^NSH5NC{`ftayc>uKduV4le@sWmlITRDRsT{%z_Z|&piM?|t1nscKw#XcNOVaxX4 zPaiIe9)CW&Kvc+a7!B2bzE=@|4v1%rfK9OLSNcnPk3cOTL{+o?R}RE>fozd)*~})h zG7_w&skyyeCZ>+ebC*EeW&&2pt*=-RNESIF#RPb@jIO0dGg}i`3JkMxwakiHP+W1= z4TR^8Lamst8)5udb(}O!1enZ#0D4|IuoJ)%@U7Hs(wsn`0G5GktkZD-$3@6$zk+^aRc3&CKPR z6J$sf5C|Tz2lHQZgHQ-npez&GERQJq@HGpRK=p_iiOg?^B5fH`x{$&fLDv!H}l_y~bs%ZZn6BH_f? z4!H){Rcb03iP$Pv{(6t595Q=D8O444kyAGFX6l6NnJ-?1nB;o(`XK4>zNsnHiwcKE zfQbtTAv`8V6|M=g5Y9+5@Iu7|Wj3g)d?F2+j7It_GqZ-sYw7C~be870s8I<|$Q?bQ z6GlcHh#na;@Ie?RbPdtX(@_*3GzyE0$06N{NE@9$zY8Bm{37~){4z94eBs%H@CSiX zySpETeu3;<$jFE(5?@=Y{Q8%6rL~1awES01ps6}4A@TV6b9I`m`}f%h>YtO-@?{=} zQ2fzYUth|>1bdGRdgHBoQA^a+Jxpf#2F~+iClKCx3>M#?R05$jIyxHc-ovj#Q(zmp zFw%K|r?6pY=;%U>M6Ro(UHwO1+oLCR*O?+$G1a-h7c$|XmKzLRvm!&|25@p*61aC* z3zR&VGd1SmBp%Qs5208NHpiPc<5}K+kdl%TW(Xx@0YU`El0%??iHnN?l>I;6 z4~tIwcNh&rp4nU5qOv6;sSSt2Y@yXtB5F}8X-qsxfnKg*I#w+|rZq+4w|L$EH!;b} zBu$-hh^f=I=)%YRg<--;an2Ukt|M#6Nra+9Mw0vcL+RFjGo>AYY?~}T*trCWH&pDT zX8nKvAMb^PtIhBw{OW%lAU)*2aEe&(<8V~SNV|6JdQ$>b>BWU&2CxCvMYi77TCxVJ zI_x=d>_NFAS=Y}r*wVQ!C+sChNEQ^9b>Yk~FZ^>I03sn`lqx(Ar}yxuhi+G7*A4yY z*Ggci(M|lB!9>CS?Kl_2LHIpbyOpo@VTZy9;yGIvCPgT7aj58UFVy(A7H^#7-wM&s z)jOXI(O0TZ_m9|(jE|2?41x0?wZfdrCvj(fA3wVe^m;-}?`~G-yOr|zG2sk6dEcW` zCkuHH$v&uiRGEua5ANv+)kCF_tmp|E$5}fred`qIt^thK&ovP?hc-EOMonS_1r$;f z8B{wG#Jp$O*(cQ0!r$J_PYv^fatY2sR8e$Dd_nT#FqyfJThLwi{A?CVlv#0qzHO&a zev_Hf9nBf?gh?AayWo2BtDUxl#07H)qIc-V(W6IeN1fgO^kDtEySoFiDY14#_ahiJ zR7`A-nPnH<%x!wYDSIv{ZMsOY;EH`fY%yzV!lA;UA$${Q z)wDJm#B<}`h2Z$8c{G9S(JH**Xq_aIO4{iX$1j;+PoHd$5W=DXja-o-J%X`!)k6^j zqNJjt4b1Aag^Pf2F8)pwD{L$f{mR!%5k7JZVvH6C6A871(8>PsR;ZB8Rg^y#*abG3 zpU;e)>DYmE51|7ZW)lKo-neIR+@F;dno7=p61XCZo`7c9^)!wG+)+KlS!z-v_nFZ zNCn=Bk55BMCo1lX7s?QK5wSr^b@t^pjdWe`WF&ewOW$>)p023%Sl`9U`c+&SrHO(R zGxY^}-Q&{I-Y@bae+PZ!zxt;TPs7+ascFg;=`DOBA0JX3A+ECd-rI`Ja8gr&z?Wu>PZPffk@P19lmLk{m1HJFwEBPQ7ANYD0XTx z3(f$>Cr%cN^X%Cj2y9^sd~t2f%+9Vyy9gah2L~YvAPdWNFiRpZD~)8A;EE&?qgXaSywO?$3NyNvaJ9IF5f=w+s?wWMYXrJ zRVRu|w$FirR)fX2LA!e?J7dx`5Ih$N^;eNzKie` z5#S^&>y}5dTVPf^dGf^c{hfUYfZu??vA1u(Vfm1F4xVH+GR(2b$uSibGDN-=*pB!n zaer~t^97b>D6UvYJIV*_Y~OA&z^*4?{LElEOKEATq~G!ZA_yC>>du>oD}CFY*%NDy z6upj45Dv&8=g$fpO4xx!)|mjII2!E#iP-W*aend_&z{jF2Q2UMob3xG1Yj7Az?E;d z#Xow~Qn_E^1uE4Dv;#oY69})srANJ+FGyaaBapmf>6e{R>_@d`4(8tPrs^SdTtsBY z3O>pO<1ql^5I;cB2*9o&l(ur^1{oEI7f9$yfByV=1V5+*%mU9R4`D(8U-E4NnoQ+& z`^V0b>7PD*6=^DV#D%W@pd4^*5;l14e=P8{kj2`_49R}@H7BqbtGGEO>Ugx@_evIV zadGqbZYvn<2o?Y>*8m<8{1rQS!0n@K$?U8CFlCkm@%$tipREMACsLb$IA-r|?%( zi%e&oNQU;v9@UKtj-{cbR>!Hh$~O3e^@x zQK|QI5OFam_Y_8O5dQWL z2#El}O5~2^vl93aw4>3$^~u12Ym2t=y=TCwEQVhPK!$yTfSHJ+xVgs~Sh|`>{22v> zs|I_F#NCgb6@Sot7;C`HzuOFs>6=;ZcoE~rNKX_?z~GwesJBJT4-4(Pi-}fl)w&c} z3KC07tdsxgrSm9=H`6C3Ecy7J=jLW4B(N4sXxuw6_3OmaP@mU-QfS)8n5u!rhYnA* zlGI7owPEy*OO>nNvM7TDPTl|Hu$GiD{M*Ns0c1N3(sA)T`%%Y=vCGR;2yJ0|?EfZr zz%XbK<_D1`&bJIaTQ(;XxbbIrGiehwb%!cg0c>nQZ2CV318`VJsmC1OD3{Sy2dAz#n`_kZmJBTTvQMEcE;_N8h z_Wv!w%ft5=2F^oLD-q+BTKM@>keAm?p4=Y3P@&&1N66YRAu`L#3~2^)6xzFgFX`7p zdi^JddN5J*jW^^U#M()%$nAE`T1adAAycepWTc6Py7+c?49&+AUW97vU*9w%?D+b( zWqj~w(`~}lDB~3qj|0vbd))yTCYMK;%){;v0_KYom`5vQ*k;@|^Dl&`A_@BZv zM5L24=#_nMyInMT1*FAfIpL_Lw{Lk!caoF8cfEf6_!_AdyFVga@Yu0Ll8&e6D-CHY zCL@QSFA&Ve>Ld3ZJb3%k!9;7H83a9?nHf)=nS{`(n@u-ni!zdQQ+1evOfHfk1HIFiJqf8va(Q53BKE7Bc?TXn z$bgxgYpK8dx0%^M;(jDrX=emfp8BIsZV#E4GDuNL3DjH{S*O-Nt4MBkj*m-e_d6E< zvio~iq@Z}^bDTCbAL$+16`J9&Wl?f|9tHG#(lYfvL^4<4N)QKs$>15 z&efyNB}VphtJi8fzs*IuZv2d|3JND?9f+*cKk<~TPN|fIIa~A$wNs}~C@E18;u~SG z0mCW6p&~-;a;MTVVlI~rG#-g4`p|7?W3vwosqT-p-D&f<@b$%v~bq74i5RydLRwlBw`V$ z&3jg82U!YiwfK4TcQ-rH_@>RIqT*sCyr-qU+B__{-f_Xn6#I_yuX|}FEOi1`47>~Foh z#25EY8TUUO$^rShAM*yHkUMgY?AX4YNWTM|vB~?H5IwCK5GbpBDpQguNZvUGCFOM@J2va z_VrX1JQ`hH-H^uX*RPi+33yG~QoN{YnxS7`F0Q(zpOuafL7Od;N4CT8>m)2U!e2DM z*XCq=R1$j_AiyG~TLR+Z$(@m*;o(@gp<8B>u0L=riy$F#JMCctFo5uE$9M%Wo(4&f zpZ`h!&@9GZK23YDPFAe?v4<8|b$FBj*AMjlBX_?7rulPrQ%_%!ouAR87P*xXiqXJ8 zm@gvIgI8IHhc7R?KRD_nkg3-8q;WSz?_&u3wLU%(sg|jyi@4GnR`3%-y8g;+peAO$tC~ zJK~ErNW)SF-4ikHvseS1EHtmDy>auV0F-dr&}$7hIW-t%egrk`zk?f`hAyfDenVJr zczhb*e6n-Sgh9Dy@7_2gkqlhsO(F^{@t`@o5-t>M(EH}*=IBWs;mo^?A% zO0gaEaSMVyy}3JyAOiVK^Rz@&FRogPMuo#1%FUbH$3;9(lE?JX3h&(F(35u+y&S>N zC=>6|O~oC#sVNzD+EY_gCixXZY^F)wOCJN*-EbIhEHTt`55k7HtA2v;a~mC!xk`6P z968d)y|JRIE4Up-*(vSgYlqM3>)$Z$3i|!CNz?|DZ?H(-BH*ubljCHJ>~g{nIc4q1 zW-=sptkLw9Z2j1*Vd5<=c4)_GW$Z>#CPo}GA@a?0)3k4hhoNdbad6Pa_E#glErx}V#~CN2Scp=g+mH$?XoJ8=_v zSz?+EX@IQmE6JP|kE(w!*`f~Bf_o6Cb0BbIt>nwS3lQGxMZUkR;H#FBM)($8Z0u)% zC*snL!o>sEqN3>L62-f=@F`+2Lt);A3x!-B@<)AVQS? z4eW{gE!!jSbHkX=;xUX)!jH)J`fdWUK@7d(6l>uU5o9BG{mR)~hP)Q&vjp`al=F@C zHESoQMq*sks)Yl|ZWd_X*P)=6Yc}K@gG`FiFE9t)?W@u=b(q=8@^YhZ^h>TH-WY~!yk1sfn zi4VKLJh!BJ;)KBXcp%#1UMZof5W}U=wYdmVY-*a)bGg6_;C&O&OC8eT&JgE8%V`n* zwYIUj3IPI!cra|NOP4MYTo#u zARQ4*wzr?j8*uLFgzqLODyoXk3Cl7>A-9_lxJg0K5#lMPmbx#-AVYy{+YO^is}WLp z6hgklS>U9U!Ts}Y5mqH>WO8zE$a!;fKJ1GKB0~m21mXs5sN&~6rsnW(|H+IYw*p== z0=T!GJgcy9JHjv|NXQ}_JaM;ghqSg&m9F=x-r!ZNwl*2Tr;zj1TJ48#Pr+eex zAy7TYAcRc@jPPGB5qYcMBYfo0995Jdc6s#Hl&uf>sM_1xhqPI{9}AsT7l>1UUxYBD z&|O-n^B9{ZG*SdluqTm-4;@lOL>P?&C)SkdC@(KxEd4^6Z))Bh(|Rf8&CRw&kBf@V zuJl_LAkcg@+*FK}L<09BqR0*op`Es&|0XqG=Y+9Zc`-uitKFqe?pJUBy=@?&0MIx30Jhu zKGP-7xzj6TSG5eRUk*ju-F zqwK7$tIIs5^UUjSDCFLvm*p_Em*ABrqY2k{PPZ=kh06nNI-)?>Y;+4)OWf=L@JnMI6Ti{QdJ_5HkyzEA1je!SEeI zL51B1UtonnN>1sRQhpvqe}aevt7mkWA=?wHzEN&-GF=xl?$JmrOX93YAXCk{a%%G3 zGDREX)2|B?k_){=kppQJ|3mDNL_$Uq;$}!lNVw51cH0u_1}Y=CxERvriF=1H3>4Lm z*5_NGQLn6A6m=XrBK!a5l+LZ@bl__2e+e6wy|Bx9iS# zBOg}>d7XCNQGeR?n9Je!tkJy|V;@dR6hy=oJTTVwYd@P%`f9@K%?|6UiX*p8K13BFEgGSq}*@iwI^LW0RUHmOz=(%t5FWt_w z7;YfmwGlcrgh+yvv~;PYN*Xh5sCnxeRyagBQc#WQ$QybpigoZba?-=3B;KtNRD&^k zLPyFskIc<6aK%txl_y0glarVt>z!R)*%U-}#W71zNz}C27GaMMeCqApd{@0b^w;7d z=2KD%3bvtc3=R%rK%mw7F#i5^ZVu7mFCX6CSLi)-kFKS*Hu#VRd>2V+>DtcD9p?G0 zEiEn1US8KDBe#So@&fP^XK_o7_;kD<1YcfWUY57Faafv;2We#xbMJ_~wxM$oo(eR7 zu!%zg9j;bZ8Hr{~i;D&Wdt(|43~Bak-Ao+lt~&2_+R?Ewaz;i*(u8n)s-eWwB>^L2 z*NUmA*$kqlH~cf)*zXJpRr`gijQZ(K|Y9>bX0t2 zWvpGtjE`lu{h3W&?d=D7j6~woGBYFWPLannQ2k*u-1vP)TQ(H3IP_?UaL&b&PD?@Km>JL zAYRe}BM-ioZsw=3V{Cx}=~s~yB1V#c4FQn{Ts=IBdXo+VA{T6_ac3r8=^`j-{oa@^ zDk4HL6$TF{x@hV9?!#4q8**^gN=oMD<_PN0Zob-}~q2+@8ae`EgIwU!eN z4v}~j;teY>cQ`qt;RxVOGoQxx$Ig(Ii{<6yh`>pLHbjYp6C99wFoY0%Q&Lirn3yq- z-nMn?n}++WXV?H?aoZTb-a^uSv?iDuZxM2KbE_rf&3`>3B4`9%`(fpH=ul|bUzdoGD_Q6Ss`E|zoJ)RqUveQ@JA@gf}j z5b`v2Z$h_-TeUpg+)ZDUd39H`%ALD+Q~$-I1b#(uKAZ-^J$~|Y6hxq#l{Z6cSgE<> z{0WB&<`EHL#{jPK<;#1#Ww?+HyGl41(Bb|Ga(_rL>o934VPj<;1tB5cM}qheC|;_b z5H@2z0)+&M-?H;SH4>vG)S|oS!e(upoF;u$o|a;FVMYIM1`@(CoU(DLM-mfM`q({i zZ}1`ypm-#HIDoGH32`Is4b2yk=LSb==3P;l;mEmQ)D$1+vh?jN;r5hZU0{6^1Oq79 z?Dx+v@I%?oa9Ws~0wQBZL{UqN0TB)2>=4n$&k&L|q`R~v{@|KCaUet^i!adSQ0|C; zIeenLD{H=R-ER8cPqQ?IAEvwr+6mBOM{5KHo7nqH}`QN za@?x5Gk7J-ix&qtj$h#bj)VhM58*TqIZJOpzvIhSxSOgS2g?ZRGzKaLMcaG6o+Tge z+Q5RE%nub~jmlI&$OjGVM|{=aO~7i%%MsJDT)AyZyHlP$3r9~pCBqd%j03bmD^-z| zmEGMNdWuYb_lK9K+Ho#OV8+JAw(U3)vFoE-6Due1=Gw=Nzl?bK!nT;kG(ulMfJdb; z#!R*vDC`ENdv`$^2s08<#f>JGEvA`ot#Mk>5hJN&B#8 zyL#UG+#YYv6PDp(MBq;adj%8URXi9H#;+0X#PtDB9SUh=sE9Pw?c3L|tnHx*?CNG! zQZ8|y+DbBolqjKJYZ}FkW59YV3HT#H%oQL`HU^d#>~tyH$pf@xD#hEz!Fh!zLho7)@XG&e1b{_XO-3rEy}UR=j$E z`l}RHED?5IVV=hO$gY02R#f{>5P&Q+vkFTLl)02(le82S-`PJ#XMT6RQkB(og0>Ga%8y(5(mt45l z_HxCjUWAGt%Qh2%8*>XnA4>EEBd7WBs-N%ojVGT$H!-GK!uTWIdb`&oSemXdy{pL zNx=&<$~0unokTSO>e#M=(YQlM)3DK}mg4E|d68Ugzif4R++NrJ{T{gC2ML@HV*n7(kabo<jS6PsVyy9c=5!io}Ra7{oNp2=myJT_R|Jo(?txdydU$8JQsqOA;6^b z)(j<{vk&4IWO+TxvUmX%Sqk1H#>YqKn%L#Vrr6HL{2BGLB zvxD^Qip5SZ%-|N3Ko~bNdwC~$v@RLbLu4talZ>tAH@J80IyO_WbSjX4`c(EqO!S9u z`2(k5Gf8%Bu_Gq^C?r3U4hFv~=Ns4;VTYmCpc7~gijebx9CqgucwvXDvvUfRoSUV2^G`QU%#DpHlGM_5 z>BF=1gf^3~`T6)7Cz6#>pDmXr^lRMaejq;z4{G% zkdrAe?=Rin*J}KHq|aZ!s@=SK^Yh4vJOcwm-S~V-3Hepi9-o4zHqVwIsPK~t(MCn= z@p=Nvpx1b}L}R-jA}e^g1xIUuhPHMFlGh3gt>-dKa=A~JM4(+9GQRipT?0g{cW{Qr zijIzmJdx+AMg;2z=7*Lp*0Wk@#%M=P4mRFeSM`vbpW5KE!bl+T#TJb(%a~&ca-|aY z5Id(r+6uxI1dIkW8B||TB+KRO_qV4+F{g>QsUYM!^5nN`!4W_#5(#)^ zSKb_6i$)5e7*b<}>__>zzs~fMvY>uN|>W>@vt=mZwCBY(kDy9sLd0^rEy{E75 zQ#G-Z=H@xm+9d5cwY0QQI4DR&f7w%3i`c73z@Gt} z{&$cfgMylY?(5?Vwf9>_!>B1KnMi%5ZhJu^ZW(4j#XI2&q(8@n&doU*A^<|X>_k7S zh_%tyG3)trLiR=?8et)u56U<9u4(7td=Q4Zz^MUR|AoN_0_oA}A+Ljjw6vsm9phy77Lc6MArBwgU{RY0UR7%#{_$DnOl9T`d~&3^v; zG3qhiWs=)V5x0CJecKC6GoX^==Bi?+^KYj`67nWq-yvJQw15A88%P8ETO$BBqD_3K z_LO;j=OW{Aa{A8OfyY(|9a}^gEge^TCn@O^vP+maz&lV3KFRgGiiwNQmk@ib>O~A) zXdn>B&qSjpxLp?@eeK)1s)Oa@M;}&rczU*D25lcde+VUcO*oxB<`@Q6Yq&me-5mP+ z*WVW@ynQHJsNMhv_htPgDv^t^r1)WR+0?i45s{Zc!hr9pJTY-q=r*aR=WA>jxkCZUv=?6}tj*Z*&+TkoR4CXS)OVK@qGpPq*UUrJL;c-9=ff>s93Hb>UHb~4Att5=UgiOlH#Xo& zv&tQHU20*r5ExvzCh=tZHRn81JbJkv0G`324AplxXdQ2I^!15>2>J^tJ_Xb+3UxCx zEm5dLeeT_}r)5a4%)%fl5N5WKED_oB!etk>P9@%iSkQL6cLS@gpZ-_Jn6D`RKa24( zLtv+mT;!~!?iqaiYt!|tD43>Gi+k- ztnXt#-TuCgoQCMvL^P1GBf2Ck*hUNPT8$Y~oHXA0;j)M7WdkOfo9}*C^9RM7YYUb|do8*; z($rL_cG1yG0_O}70tKW9W&RV}{_2rBQZ-#oSKt7$VTtIc#Z@FHhhCHhhJ>gFhlJ=7 z3j*9P7zWyTE?-D&!PV6|1tq5!NVN_D^f6z>3kXRn+i`RK1rc|GokQF>=pXyArndID z#J}eC*({f*-U%?NXx8?zKp)ErSyDBHB~x_F;_t8}XMr@b8$xo}XTR4igMeYm%gY1dHLk^i&Q#RYXog&rG<@Z7dflo1 z+yZJRJA3;trcC+Cxx>NBxnIo!!q)IBY{+n_?{<<5UbJ#twwlFt0 z7jIlxs7i4!(8{k(S9EW?)rH&^AQ?cp$4{SfOBxK$a-d1!kpP;6aA54*-r(*1B=Dc= z&6_r@?{hq1@Y7{8NJ&m_t(zfLx9$oG%YsNUC|`$`p50RTcKe}&9b5L2mHg!?y~YCr8#XxbNe?{|*MK zbWT7?XY1tD9VVPF@>a4Rv=bQFH#LC8GNoY5H_pr~*}nabCdvZtwvoL({$0R-8>)PqMM&!Ut2T1Lhgf~#2DrR z-`3V{n%-@{$59Ja&qzbMen}vE*)5kYo@d6K$qKVH&?;67HZ%YdS`r<^ce$bepTF_5 zv&+=Gm>M8NH;srDNg-Djq%6CjBM~T`el>%b9ov&w0%gix%QsT>VuL;cyCE^5`^aWE zuRx^JmWwV$cNLGTFU1EIDZ{bz$zUZ8rDU$I=b6G{g~5qpGUtqYXeOoTYpS7l{quE~ z<&OR?-6AblgTfk{n8?Z}5QhPnI&j#m$Wk5eAj{diDDVjv2`W))yObzf(ax8YMOdB| z?_-J{V*7~`%0Ri;>F?&%s_!(2GOP~uiZo>ggX`IL{JFD4DPp_{RI_$2j*d*#Gw}Sn zi>9W6Ik9cN;Rp0R|MK9rek5hr%UY*c*(!Xv{Y;lTE^^WT#qw`pQxV_G zswSZb5OQ=UC#QZRJsqvZ<^S#H@4p=7V#CWfe7WRo7;0r+9Ieobv^4RO$!tF+ap5Pe ztlnS{)%$#MXN#w*p|%8qYhbg$=0UB5Hzd^7(s(VC0Uq|BI;lki*(}=*9jXh=Mwd+; zB>A;F1>BdJv2P)o+zM3$=bQ#~ZKx!6f!xlLGIx{!vrwzf8v3!DA@%UKVP92p3E zd}!sy_3MKc4CfX5F|(#joyv!#0u7SBqH-O)7IrO!3^h&3XtonNI>7% zm}mO>W-XpF*cKE?M3~9r5-OX@$`&455E~!=U0`k7(&lw%AR<~`z6^oPLOa#S=B!Xm z7f3&w96+!9#~%k&y;K+kLZ`kKlK^D>3c z9O^4kt`Km}P)8OV?mY;i1bkbaUss?3*X`4%$W>h#=r-DD!6r&X4X#|R zqJ%`}B=F#+MoyYmsU@*OS~EXJf$&vnp9!TGooON7fN*N=nPz%Q`fYoe%mh!%)w=;jQZ33nh0qcq z@NPsHie;;qJ8H!e-go4;DQ921t}UJ(9i$!f<*5RI`RyW-g8raDh^IhUlHBwA!lY*I zFNs#8YHMJq2%9j)y5Og%#nPwDt8MVC6KHzW0?jA1e1O zyW?STWEC@K<@c)O(`!cVA{Hn67CnD+W_y(4DBlLYz(>TH9G<;Y*B%4tmM@N+HS=L|Oy|8xmKF9kDZS6!H9yl>XB#CKfb)Odw ze6gxKjgy&so&l`}=L(!meo(V*L~WnG@MmPpXqCR#~QtF!hAdZlwEt$ZATQ^~X(5(5z@c3mW}FJv3<=0`Z>GoUXg9 zTyg6++hYn*9_;&)X&VY?DDnI2g*(kM7efoxLOzU^#SO-Qlm%Fr7^fQ(`6kqYa-h#a zl}1invOqe-N&x_vx!<#&&-nMU$%t4V6Stg}5vdYeuQ>OKRggD+h-a<&1-<2Q`>eVT zA3kVYD!qI;b%M0s#xcIKf|pH-TX7F@>R`!P7_*3Xo6#$4`1I@Dn_Y2@tTpLW8nFBz zrPd>ZwyRmI1f~bj@IQG2`TPgjFU&h$nE$$GkJQ`H+T)6$3ujPZORGazyN7hKmGdUsc*J?j7w)bOj@0_e`|fPO?1%GY+S9^A>Sam(}5 z6(%{DDK1J_B79gfYu=@`b$xWq{n`8f6+7QG+(@~DM$c{Z(St_%X&E6ukEiDp6au35 zeX=(zDyvG3Iz-mAyjSJ6{?bZXQ+om;gBrL4X+{0zq$+pI@~0y$hJp)B+J_G+_rkS=scM ze|p2*n5ouX2(VERjup~OL;ycvCZ?I|14b^qnUbAdb9!UtJhj8~?J*to9yoBCv`0PI zgQOf@BPaKF6FqZxN0Gct0RCS0KjKL&og{AvT5UG%&0lSa3=S8uYKuztC!OjZ z2tqCUrekF&gTHe5EpwjLwy~**c%v2!?_aU&=h91;CiPQZW_t6uu~3~)J|%ZCH6{uP zHS{dF>-%s_aCNM1D*+&5HXXnteG>9J3epHgm4DNz-yS2bRtwC_&ku8SU`^w@oU=5) zr{dzA39u1a@RD+?>rifZ`?Kqva1GjVM^ z@)Yp%7f4t7&pOwg^A6njHinN=9AyIM{o!W7hnuMy`-Yhk@ujsi-+v#~m%z}0W3x5f zM``En-UdR}X}Zn(mXM-vtY}X{N$lit*eWF7J;Wfj4v@=Q(VKrSN4GW;?WD&Yf;+egyLT}>m=ELC9KP9 zRR=Du07t^OA++kf-sTv2$B?j%*HP?<8#dU&!;7dmBA9eQmMG8s9JylhXLbWX9wS17 z!R!ZpTRXW*vS>xysodN{cQ-v6fDC|Kd|S9E&y4nZGh55U{I^N%;OfehvToDO*v}bHW72H=74XdWhH>0!)P36t+{~SK#$RRUlFllbrjjlqm*Ap`{Zd7#>g| zoVw^4@iM+A>ac{3+~j@YX+vcMmknMa7Em}did#Yk#&==TV~B4q21})rlU8vP2;2Zu$Ow@W~P? zO?{}#tQ|X4j$Y5oa4WW; zK+k4>7N8BJ!R@?Fy%23}`;_7;S}%kz1odzRPmOEy$?b+U6Dm=uqq`6{CLFA|fnuE# zjC<}7;RWJNh719(Q5XITN0ao7`y=Kd#iSOLKe{$R&?8WZ#PG}jYNUMooF=LZRdnfN zn^d@dyJ7S$q=lgB4XeM8NyyLG$AaLo~XR z|8VudH{ked>(6U*YFtCbc!PPe6{{!O&zhAs`MNdNuJ(Y1MAkXsQ&_Gz4X@?#on{e1 zp{+fOrT|BxfX-opUcY?i3KlsOF!3m9L}hD)lOen8HKLKh0&vfIMMs+h%#{TI?21o4r4#$dP&1VYA0 z`ay_^TxxKPvE0P9%xXfeP#)Zrdm99W{Q@ln%_O%rGrsZ|cSkqKqm>MtIxQCML))4$ zvFAa$XuzXG4>;=jc}-^>6cGAHTsCcS^n&4Iy)E0;Oa$0H)2bNJ)yhIW#3L(p$#5<8 y!nGiDQj4d0GO75cQFVA`hNgPRMZf;-M$>Zr91aFI-Q>tf$=q4g+!u2@>7#n``ykn#iYb?sk`M~I`8hO#g%&F+C7Y7)SEpfM;)gbHH(f6**%P&Uwpb} zFC{m(5PiAsuKh)HCam6$S_ev4y)$(G{Z#>f<}H_^6Y%&k%T-Z!R{HhdT3Vv$C)E>A z$Iqmm^^hlMXnX{$KAIjH8yh2t;NW0JKgIi17x~KBUPv7%QT7-dy!i+N{^VV(K;^X3oj~_q2eDg-p(ecQ> z{rgXyJ?quba9UJM?1}Wr11t_Z$bsEIk;qqi!NP*hPm%JK_QoAMc1TD_$nRp5=ijOz z5bp3wO(6Ujzo?-&JN^2rqE7^@f(j+M@197!Ym}yP=FFBSPoBiJjB4D?eD&&;TB|*M zPi^7RNcHuCf`U1Dd1alQ91{~0$izkaQyqvQSh^*(FeOPBWe2L!}7U85ir;u)VleL6Ke>lGWzwYZ1`V-L&7cN}rxGQwMPf<1TbdlO+r?20>-D}UbvD^Rj+c)iw zB9|!VljUV)LKe*j6qS^A3kx#~2ngH>mwuK(>@cCGrj~G9l}Mkj%9hk}x z*+2Z3zdZ4JbtcL5^P_)g>FF<8j50klOOrf&cw4xjv9gnsB>nnz6(L+9pFXMLq8GXf z9H(Yx`tv)Oyr^4`U9+~X_!zML!TtO0@2=Ew@83_i(TnoIg9pBWfghre*a=y+i8jAu zzl8O4|KY>C)!~9XM~<+aOEV(3!Cg;JrX4#1A|hB7RaD-ck>O;fOQ+GoBC#o2T;J`s zCL>^&cdxlwM^RDHr0U@w-5lH9+}zx{lm3V5o148KJ=)64$JbXADWZD(xQ8ll89pxk z=E!O3UmvziO;7jbs|S=*z6rtpxIWf;Xy=g|RC22eJUcl!GHwi<_)t+{y1Kk*d*eo5 zzGB5)JiXoj{IlUo-P4a)O7W*(F>c%D)s%eBtm*Yxtj&RZ#efpZH#8|JDH5*B5_1!s z0W(8&#{|O720n-B7CIefIiO2CQ2pTGS3~=?t(CpT10^;5f`XM#Wt`Km)NyL-=$PV_)=cv)EC=N)h(d2?4+ z*PZZ+Km{cwrG?*(Cx3mv5*v>aWYPSlbZ)%;kadSdk=hPf-*}Xhwzrq)Hh3vK5xPLh zAz|x&Q<9_m(jj^#Ci5)4wqiFqY8skQE&k_MVqG4eP*YnJu+U{~qIl6bGJMkQ&lbOr zrqjQE#k;MH8ebG*T@VPkP;<@7D$!+W?g91*UUi!JBCfLHZ~x6&p{vMc#||;el9i?T zUvup?{a)LR+=GHP;ltF^@S(D+3ueoUb#BV?^2FR^cgX$wj78ObA72)5kE(FF+{5Bj z*ca9}6zf(|Em&MrRvq~J_f1+VO8dD5Au|h$fbO-``5ea?z7M8{UTDVn7q8By-3k8~ zaB7>0;ytVO_q}1~j7rIg;&NS}Fslq6$bUnzmyvcCBQ2+swA}L4I>Kb4BbPxYb%I_y zC854G!|eJtW6i+ zN>L%b)55}{0Ix-enlm@QIlsQ`X))2W>iS7aVO~|>**OcLj?O2SN7A*oB85s6Psw*qR-vd&Mc+rkjuWF*0&w%wjzFy1~9Me=+M0)w#L3 z=i2+sD}y-{6}8WvRl0utI&avCmfIpoC9F9pmTY z^R9g=(?0rpG2MCI`o{I^ha6*6-kxGIaa)~o7%dUdl7V6x>!kFe1 z{T8bzJm%BMO^V-~`F~$>QdHz}TRub)mu1nic}Xwd%rg7V;TtvSy^f8>#Ob6jE++ZU}0ja?<#cOK%hOaFAIavb6yA3^sedOs#ElWp6!QMn5k6?}5|=knsx z(iXx$C@3-9$jMK3X-wqvmoJCSMO^;eq?B(-GoGAY#xA9lr=XzdNPnsjFWAV#eZ#?F zFYzcc^4}-dVQy~Tk^cJiYfhi)i^8GTdH3w8pB|{L>gqBDXIKwpIZ{Sw!M^&j*hp!EBav&pFf}A=6)*bA|6*a`c9GhMj)ld3!-Crn>?b;oV|_i>;-@82 zbTjVyuG*Y=ogH<`hVGnA;}Qzj1|mf->so6|Tj)eZXG6_En7DCqIzQ4ONV_0#Y zb=#G`;)T9|1w8gsXU>#kIivN^&}`l*fBg7{wzf7cW8;v?qNUA5j$Oi2w^c`?q#;r5 z*Fd=Ovz#2(^_~=xF`JJZIntW%Ab7bpx+BTqW zF%Dfv4GlT;^z>}|K5Ve;$hrPCX(bK_hP+xI{u|7H6klrNx;bcW&i=^}JH8Zy+#9Wi zR+KW9m#x0P^|Hvut;^axwrb0K)n4fwg{3}EOW?zA9oc&=r>QMBb;78fhNH-3$^KoV z(YwoE(#Jg5=-2;gN^@1R8>$_j?h4W_ALU?G%+1Zk)44j@oKpVti-xA=iz`nZy_Z*3 zj`MGQsJ$-{)7jv|<=VQ(GW6lYt7w&EN#K6qi!$tW@7~v$Iysvg-%ci;uE%b#YH0~? zrxzBmEYz693zPO-jkdtU>6A4lLSIpvmC&?!nf$V*xEe-omJ5`$wYQJt4n5`Z zQaCz4**%mWy<6l?m&b0~iH;+0Gcw{eqQtNQ@W&TMUL`%{CVsCjP0ko@Y*f)pc`Rnx zD*yid`cE>V-y>_ds=c|Je6;S8Z&D z@})07vaqqK9BE9-u>3Bp9xKZc6cm($tpVucd#S0`ub(#TO8-FlW;=!_apMPV@XjN5NuNb=uW;}yXQxYdeVLkCfywktPzmY7Krv+`cr-OL%dqWLn42+E zkKMX;YY%2eRb5^2^l4^M_DzE|k)Am@5^waf{FgTKHA=CVFrbF-Ogb5>te`;2yk*NN zu$rD8lLP19Qqi#-kiU457p-qWAe3$W&!0a@ppLE6`+KAj_400L=oV8`Q$~PWVB_-g za?eTOg8;V_U;o9e(XuY=etv#A*ZbFFi8C=X-^GNOVg$ba{_GEmk5=6b3k~)B@#CUF zq0_c=sRl=}R8ff;nV3Ah=(d}p(fIoMx})TEC+bPFn0U%3)c5>sO70l{GdueAs;I4l zg9;X8Sy>sLt@qTF?ZVR1jG@4cyDu$D{lelE1z*m!;R=h^2kUT}jCoIihFh?O2hwTIFQU7dFGW@RjpM<@1l zUlQT?_U#+VDeyBnE=yt{Mt)!}_(z_X`9j&f4IL-`*|%?Fe0=;HpTktT?!Oe1oBDu8 z`79;_1L?uF3HQ^lev};$5@I}h^eC&i^-fT`U1292Q(Z4MTovWtw@<;^THwZw8#yJP zYipIQtPT?Lz~2qek9V9Hs#oFq`22Wi>#M`k7D_U#Ga*w|7X-DPD8 z0?#q`J)@%mB_;BqVXC-eX&D*Er(0g|u$ZtsOH8B&ir}L&0LLW>q?VTZ^z@C;IkZPG z2NJD!baVjZZ3K6gIC7*E1fL}PH*fx!&~IC13sUw3ti!%KmU#O5{OHf0pu81cXO)zw z(W^0@OVf847#IW=TwGi78akH zx>-X*!|R-n14dkDhnMo`R+^c=@f=^Uj{8&=s(G;D8tgLODHf=Jwo-+1cXlKX&Zabq`W-DlAf~OYC1`5AvqlX?OHl z{nZ>|=<)_ts8fTSLe!)u|`+OKdK%ubPDEJ%g)GP`*1FZEm+t6 zkmu!k~W?JVp%_aSiofszOck;^r# zKZb_pTPwP|xvvxld(>1SoP_0>BP$G*y;vUT3ym9Y6{s+}Sb| zGD%!q-0s)DY$Li1foww9gS4AAdCBh@o{o^;C4coQKb_!Z`3%Br{kMvs9T%*uIxpp* z{(v%kI;K>kS|PSOlH#n6&Uzago13e;8>lEBJ$i(N5SsKk;(_lhMmI1r;&=Yt<`XLl9_=z^2$g zzYN$!8qzsgMS4(u({KMWrS($4*8!t~2(RrT{Ny4r#UjC*@TFVqD$_k6#PjI>Bqi(W z$W2Ks=XC@qd3{^kMpEtSYs<{eK9-_0FYy%0-SACGLSA2ghj>9s$|hsCmBU0yb2AIG z-}A~}{98AMdJ>yAZ)T*W`d9KJh`*{@lxxi%5oSztd9-Gdr(VjS^}eu;=w2ODq=cBI z_fmTwE-QNY@X>^N`Q#>rg!(u%Ey4@!Dd_)8UVDq zlG@tMrWve|Q-EWjF{13cE5wsuo}TOIsxAamw=#Ymoqd^-qNJg*32TLv0l_3uOYBN7 z7NnhirB0cgnD}u_f|~MZHeI|rpC{_T){WGFXTT~w!^5;CnL`cwbrlOa4-5o+v|3$~ z4F8IQc5AVcw>A=_m|`8FoX~4O5ryIyhb_A%wcg4`MybEQ;sOA|!Gi~(X?`8KdDYT# zOl&z{pFS`x<)D%W1+Hbsl`}W(nZ(RS+ zA}8&vzw5f+YUt<)1dM|c7fGc(R9xXAL+pB>+SA)haplUDP=;juq=BKKhHODaF~|Hb zp~q>3g`LmCtqeTQo;`bu%?JZUpGXzou>960-7N0b>Jp^B66`zEjEKtIovzA;?ys7z z3B*m$%$$Ovcq2JAb+GLO??Y=jEsiyea7IEUFcH+3fB*ht*s39JQtM+dQKXvL-(S8m z3zaf0O%TdzycYlM=!AH2?se)ZIy`&#(g4MOs;wQI7#bLe+gwv$ z+#KgEuJxC1lh+jxP)0w>o<6*K5b`U!NlP;t58B636O&z(l$4A+ch+=r`Ndud*d)ZQ zfFHH)%p-+T$PnE46g2UduU}J6sbzO83{tOOZwgp$pt|_yPg!kk@KCNvgilh_HI2Im z1qB(v5ip<%P>h^T4s2IoLk03P)~#dOy7k`iP`=W-y1KDF_YZg|QRxDjLX@=~Z9e!s zDT#-NXB|`sW&9!8VEg;c?1TD8N2})!A4<@3c9w!-oNxI6BYO7oB`r2cdUkf@2fr;$ z?Ck!KQOMR0vE`xC7(1Ii#S5L}>nne58RXk<0;c)&=~GYYyHxFcx!WZ~MYjTU&~Dgp zK}w8mkOCEeM?@rabStYA?X6q4u$>`h9z%V5p&t1cg`qx{TZ=quApn?FfV)x+^SwzV zhAU%Mc5zeD(3n9eHPG_%_I_KPAymW2fAFA^vhsQoDv>t^sDv4$^dP`j<3akg{&E1)pNO1K0IWMUCZm6N`LF@mcnfm&Yu=2&p*xH!eRYLS@0G2ridHRjB z^foy=JA-z3-XDQReEuw9tC5G`?? z68EgdzcoVKhLZ%eTef(*ySsZl($Fy^2pz+$D7TvcOH-Mfr_d5);db6De#yoxcv@LX# zJ5UROofRMf_Vx9p+mGwryLXTN(@oBOC4fRxK&|~H9_v2U)O>(Imq8MWj~_2g|EOAb zdRMv7V?h}i4j%@tiU&L@_hVy80TI1~B1+uGJ0PHXUC6u#<=EhtsN0i;^R`ffKV1}- zp8a-4H{bps#xhspB}6YG`TY6wo~hn)lHk|3w)&n;*6D3JXY7)$$uN6NPmleeVcsL? zAToc36Mlc(ZmgxIrsk$xx}W$~cYg4ap14gHFY#k^R4QF5$mG~!m+-oT+}ubAk#6;P zSjTrUel-h`QHEBt!mbjl+4J(%t5T6VX-`n-XQ+mdrR1+&+xOJz=Rb3|qK{6MGsqFd zU~Npb-JWtE`CTR|uT@wxbOS+ndr1)#0-@HaQyzG8AL#KhLqo&Zih2w8Jy=gz?qC)Y zwmk&7aG_AXWjG_~`?5XY$E-KC?wU-^=$9$AU5q9p4T(ASyKbEo`b|ZJdsGg4@&J;F0Q() zT#yWkT_;c0xyohB&6vJP%gPGtx-+9O{rflX164)f>`a^PB5ULPqW62bNiF+Jj8r(f z-}lzmuUJ4Mc(i-MPBf)CifFcXq~y0aV?b2yAe;?}sXQvdjKmXZ#~a0?&8}n|B=B4c6<-Paq+O623@uQSuEA!n$ zU9q)~59%uuIdu+hKRXK??P7n91n1UiRJI67OBYm6k!tSc%KAk?D6&3(T@J|WNZ+XW@vK6Saw8&b-H?)=7VKTuBC9i)u4!NE;KLqjPq zw6I9j_6CYrf`&^?NXP{jlROpLS?uO6m|d-;<8-ArTnob&v|KpUr=Yqa*h zZ6mWze@2pGuR@@wayN1w&vGpkD5O>#s@%VSKdEV{@;(EAvc7%m)?o;N5NRNRH%&Uh z?xlz$)%<frmOaP>alWR;-KMd zaQ`mwv(%Gj1Ia^~m`-VFF;c|cyGIpj50`5Ej60jS`R1JxU(JHxVN$sZi-`R9X~Q(T z*zo@O^LzRcHDB<&PsYl|5MO6UTk^k|T5>TmejRcgl~`GowjLX}v;3>FBfWTSWs=IB z(|Ig|=5T>hw9L%R!ry}h z68Civ@C9xU(*AE2fSVh*mr@?eI^Q_#!arM0Dh_8WCycx=`mfx~SH3j;?}|oQ$j_WK zcm2~~#QlJgfVRvB9Tgu319CqzEtP@(1J!T1&(s%PoO1SKtQ2uDFRfc4Z_pAeOWkX( zaZZ8;Ir4yohGN~2gG4R)wkKR)Pr z`jz618^Y7m)3$4?E+mpTk=XDfd*9L-8_0YcH*U23)u%Mpk-G(}8qHS1Zjk=H<@bi6 zHi+;`hdYJ^-4^M5X$6ZGxZl2eSKrV;$qko&awhYj24KhCyLU0Xny1PcR_$U?w61(u zzG3G8_(eg$LUjqR)O;$vfdDF_Bo-DIDG1oVrVXhxYcMnR%E}hCi*?4VHH8n&T`^i8 z^(!Ecjg75i@%*4Qhs96xF2Xix5(H^JcQZVsH-`Bvgl$g=#ZC!Zf=IXSlnm`|8ar87 zBDh=DVZxvQ_7W-Ck!Cm{53mqx;j9I4NVs!I+3yk(x-a!$x$k3ur>vDMsUl8x72fXk z+Fm0r)N-luS{B(D^a^fY57*#R^VT%9><_j{Jbhdxgfp?CLiw7d<#Rle(1e79s^Cev zr7-FW=sMh4+v08Yee7w z-Q_%ay%BAFD+hr06MOtHK^oJ-~8C zRh3p|ZFz=IW%-Y=4Vv$J>&_EJMMZe^&o&d_JI?vrC-+{SPwWEJbsCJk@(CsFp2BW; zd`~2A?Q>b^_2HB1q1j&oH1`PJ3fC#Z4*4+HH#WAjPtgmUj41 zfv?jBA#Uz0Jq@fi-kxxtgTTb=bcR(;I+lHdgI!<#BB3OeJ9P3Dir0Y`4phfTIq-{# zJtn?3o|MyoXjUkj)FNny$WOo9+PvHK-ZE-rgm}<>mx>y$zC#*;lzCwfUCUypVc`5Q z>9*!flxzXW(CQ!Tr{yiDry*e$8Y4-4AcGj>*itObje8mhOs-U|99Q)$mB;&@1M`vv z7mD*4L{ks`y(=jyE4AMS7dg8>1wf>g7(GUg>9Xf<6m7bAN3LN$8XL4E} zTn#>-0XFYLf_wH*rxi?Zgh%vip+Dpp|JFW;RjMaXk`n!&l^vlBD+!#iawsJ0iKVopX@CMOW72lx7LFf34u4_zZGoV1(VegFE7q@s=TbB(YMwaJ z=Q?JOr4k|QA_nfuV3Ba7^Hd%YwH^v zV>XG|wtYJfVkTq`1*GSGWaI{JlI{RzGeO!XJpiccV>H*3N zv&9P@`q|c`+Dt&|4aUmZec%8+GEs^ECg?W3!^5BKnlOdrEQpJ5|Ni|u$-)(q-@aug zNKxY!JBppqrO#WbsHmn4vK-6BN@`vuC-*ngXIpoceTfo(5EiF?nGO3z8Rs?A$J1UMggw`1FrF{>GI4k`VFn)za3!IDPrj zl`A|L1~N}qEi634!nPrsg`^mRv9U3hG&BhY)C@9228~*go2mOF|pu1eht9QqJRxz!me|2T4^i9&;%ABonWEM%F5pU@j#_#WMl)x^4m^MWss^kv`oD3Ax?Jo>^6jK z@N_-iz7>WCVMlTHUo#;yD~nF9^d`=JvI`+??J8VG}8cc=%%j0|Ol^ z7;h+pft6KC)r_U3WzX0cJybOQuoDRQ9et&Jqa5mAFFqAYC#h>fh}!6NH>TBMH(c{L zon*wV;!eLJ?Q^V7Bt@RRc(MNQ;lre`33d>PS7(+gm!< zJ?Bo{NI!Hg4a>g6?h>@i+>kO!0xaUuog&(6}OHo zU29ug8Sc*B-kvewqjUjt`8hi~5g>-2qoeVSBVVBoLWqQL3u8)DOpG*nP@M5KJ3HI4 zQkz{-Q6bQu{r>%+j&4QRqvYh|suODDjbg^(uT+=sKlC=8=s%7{s=e=Q8ePDz%LeVq zP1hhk*{K*gKl|5(L7oy{4^*iDU9GpAJHTRR;ozk}v44NEHJ3QrqRhmZLzP~GWcXJ?>Qpm^fx z@1vp-9+i|ecW;dyB}Hf`(C~6_JCJW7RHNy@EP`bSv7B#r!?$lAteRQp=WosDoT^;8 zJNSFG;oyIL zmUW3J6u1r2sQFKGI)A>(%klhqHqx|#o*|=xs&`>q>u1QHLl*Ei9bk61j-RJ8(vE)t>CY5iYXMNDfz0r`53wX{l77(tVB z!aP8k0WA2`BTBsVbahz~fOUMjj&$6m_rcpBK}kcy{U=ZSkuga10lx4A&_d{%qQ5dk z1@^-z8$C(J1onsIJ4`;y%-mWc*ex0%d}$*o^FvHjj})dx;z;_Oj1!{K+@S4$V-btf zmkjc5ZXol?xM9%mL$1rWt>eiz0==}ZMqYRkA5Q@`+2PN3@E~ajkmv$^l@$3Qn3~Rw zeW#_P6It@Izubch^Wwr}SO=+%oD#$s(1pu7a_tV;4XTqP06Ozl^#mDMLOH--+(xy4knDuYnN2N~@|iAk9%(7nlllfC{kmD#wmlXw^gm)Zn9k!7cpeRhjM{2OOL&m`7L>aLVsZv#1nBq~ zPrt7-p=eft%R|PmR#)eXd5~s0{c0;IwKk_2hk*Zvjv60Qw*h9bU0rtEDS4B&+jZ$6 zM7IpwQo&Rioo>PHjPKPqL<}>CQ6)1oo}z_5x@8FPN(hc1T7B=J{(DmPPS463Kp=|h zs=0Y76m&9!O&T#cKG6Q&svPb%u)?B%jjkC*a}dObvDS=rW&Yb~^UehG;P0IFdIw}o|Q&z+kw zWET01?~Q7Lg^EaRh=LIO`BllaC}6I8!TISgwKNORLUO4<6e5BBSX)*A$2Qa3Lt|rs z46+LZNh2c;nK5#31Z8(Q1>_sdzpQk)JDrl5`3MX6IJ4h9*~K4Qj4UYRkIg=ouE~T? zb)5Lr(&AteVCpm*;?j&vu!656|}Xt0#Yvu_?=4-D*^m z5x60}aPS0#+;dz*%9#fnnO`NN;B@o-aVVIEtv~s?Jyo8p~ z471A3_q@E0az7wx1-K0w=Wc>_fkF2;oEyj!)2@ zNz(Mfi;CPwq2^(Imu6Mf)F@&chzV(wRZGYs;{$$k42OLL!u#>ORE{3?IG$fyH=-L* zYEpuVc<9zo?N0+Yd=-g)hOAn3&ON1EfA)r=%Pc7Sx^Z8U- z>Op+PO!)Z@Lzmc1h@y?;xvoee-9df};*ffOlHxsr@s#p6a-(rnLk%5_G!`H*WJ1tL zH3SC=p<97=kvn3XZyyA$Vgs@AE5vQgzKsK?7AWN>3uZQ-)z;QR6r`!SxdCn)lzt@_ z*G)+pQOc#(zQ0HHUpYQLuMFE2(7HNy2 zeEN5ig01oK@l@`lNQ*8T(_wXQAtY^kzl9 zKG)QUN)_R(%@cY#cncJ9$gev{jRyyMY~Qg1h2b}|3qIpfR8+f}#^6u%lYVdL_OlWO ze4&wnP#^qY7ioeJBA2S+bO8j&CG`?N#IZliGj)psW}kxc2f$6K|GxqAI{|+K=AW%CMy0JiOTVV|D#Nhl^N^p?ipsb%_51hp`EIw^Nn!7f zm+gL&0|Q=U|CTC=?1Io9fwM4i8a$Gc>;POjw|{XXJMM?HCNLFF{j5jX9GSVDmw(UB zCft6t+IW?cy9_61d=Y2>xO4Z#QMRSST*rlxh6tD>K9Dn4Fsh4 zKq>!gqRw-cq$LVHDzwxjE-z2=Pmd>qx>)$q4EvlzPEyidin#Ii>@$FhhsDLACKgmN zb@g6eoF2$Tzb>lo`8ee)?kx{V25L;?`1h$-GnCJou9>6Rbxs8M1qbuRXsRd{|2_~T z)hgBX*HcvG-#RC8u+Zov!U@CndI%Bo5I=tWP(;VaU?+Zi1t*K!C~ zW>SR4(uQCBkErM)*omcH;ioWM(!ZMAm$@E|_$t~po}9O#yJ4YI7zXC@yI$o^ zcv)2Mj5U1*D32ZjY~)}8$`%B!d>w1g4jE062~2wGem6o9A9h`2rT!l5iVmt%4TXE)V| zVK^JYOA>VH@ig&pU8v3RaC5pS@*uoURrGx4t5BrHKVsR8|=RWG<#1BIJB%?8O2hCw459ppldJK=}lq!S_u zIXMyJqeKRgG@VHMM-}YPkVWJKRIN7HLJ0OeM7GhYt02-)Hg8A5++A-MQvbx}>A@)| zZ-l!^7$-g7VTVxJP`>D8s@FiXekyl8o=y@AE7667@Bc3 zC&P8c2`Tb>E0W?fTF{(|)>fUNlQ1F#;*Ngz)Oq5_`)6aIIxBIFBcw`Bz6eR0%s;^u z@PM*xhQlK1Z`o%n6(eNfH&#OPzdqG-6m}&&iU^qy3Oy<7hXhMTn5kSk;Vh4-Bh9(Z z9Fq5-%aG&|OmqPUKD^M>H!Z216*&g1(GNsUx{sPMlB6aGiE$myejGC}*!fpLuIC1& zA&^%i=>j=wk}Kh43;4<3OHtFYm>@+_XjI|FcAmuPNSQ~=xpD42`Sb&1{M}nO9=cMy z^ML+)deRgvE|%-QM8?~?c#RWl3nU&{coHeX{|fT;rF|bMR0chc z%;+G{zW@|_ zxH=iRLx&)pa>CFKAYJdqaVNTDoH7Q_q=6VuxGru|Hq&KuuJ!Qn82cnrr|Z7y42V4+ z-D#X(Ms5I4kD@2sBH!83k(9;Bh&g$%dS#_|Xo!YXsU00NRt~Ni!?Gkb4kM#rXw3*3 z^C0|3YUKR(wNoUZIwuf^g^heF%TL|C*BD`Ipw1>u3SP`9?Yw^ z?ej%pT)FhimrbM)VSMGvb78qKf}k)X|6YJAWKzDq{=w2HQmU`CKlew^0%&Z3I*U^n zSEjSUf3c-V<=5Q&A2KM9L&M-|6S>G=(m9z;?I?ExZyWo)ovxhH@*Y%(A?uj!KVY4a zhx7CD+AhY6y#);{Q|EqQdoBx$4Z0C{p%*kvm;n$r2^^EZF&~8gxhNc2l}_rt#Z-y) zS51UibC$s6AO-&$faNO(1I*z(+orieMR)y?gh*m$Q9jN>L#c_|eoy>wo@Iga7>12E+)m=0fx{ dyH>fj4}D!{Tc=`)znFnIuB54$s$g>We*s~bpfdmf diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma new file mode 100644 index 000000000..d940b97c0 --- /dev/null +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/connectives.ma". + +ninductive eq (A: Type) (a: A) : A → Prop ≝ + refl: eq A a a. + +interpretation "leibnitz's equality" 'eq t x y = (eq t x y). + +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 5ba0b08a6..a12f1fc5c 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "logic/connectives.ma". +include "logic/equality.ma". nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }. (* This is a projection! *) @@ -49,8 +49,6 @@ ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }. interpretation "union" 'union U V = (union ? U V). -(* ndefinition singleton ≝ λA.λa:A.{b | a=b}. interpretation "singleton" 'singl a = (singleton ? a). -*) \ No newline at end of file -- 2.39.2