X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fsd.ma;h=acdc78ac6533de4c23c51443a9e7a335b3dde4eb;hb=c9a1672c725945b47f9ea8af3c23b67cf9026f01;hp=0c899ad444fca856e47f68de32d0cfcaea081996;hpb=f62eeb3c7824564ccbe4fff6e75ddee46ca39cc0;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index 0c899ad44..acdc78ac6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -70,8 +70,8 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) …. | #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 // [ < H2 in H1; -H2 #H lapply (nexts_inj … H) -H #H destruct // - | elim (H1 ?) /2 width=2/ - | elim (H2 ?) /2 width=2/ + | elim H1 /2 width=2/ + | elim H2 /2 width=2/ ] | #k0 #l0 * [ #l #H destruct elim l -l normalize /2 width=1/