X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcnx.ma;h=ba3c976ac8cf7c5ee9a69200b15071c5ed9305a0;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=43562dc934674d7294746e340f673f85967fdace;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index 43562dc93..ba3c976ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -96,7 +96,7 @@ qed-. lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄. #h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_ -lapply (deg_mono … Hkl Hk) -h -L