X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flsubr_length.ma;h=db04cd8fac35b21ace48a49f7ffeb11b9bae47c4;hp=e240002bf39a6fcaa70321e550b4bb690c52d922;hb=222044da28742b24584549ba86b1805a87def070;hpb=93bba1c94779e83184d111cd077d4167e42a74aa diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma index e240002bf..db04cd8fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/grammar/lenv_length.ma". +include "basic_2/syntax/lenv_length.ma". include "basic_2/static/lsubr.ma". (* RESTRICTED REFINEMENT FOR LOCAL ENVIRONMENTS *****************************) (* Forward lemmas with length for local environments ************************) -lemma lsubr_fwd_length: ∀L1,L2. L1 ⫃ L2 → |L2| ≤ |L1|. -#L1 #L2 #H elim H -L1 -L2 /2 width=1 by O, le_S_S/ +lemma lsubr_fwd_length: ∀L1,L2. L1 ⫃ L2 → |L2| = |L1|. +#L1 #L2 #H elim H -L1 -L2 normalize // qed-.