X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq_drop.ma;h=09ee8a495c68c1fe7530e28118af8a588f3453bf;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=a2df4662042329d87ba600be65c0e9e201b040e4;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma index a2df46620..09ee8a495 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_drop.ma @@ -127,12 +127,12 @@ lemma lleq_inv_lift_le: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l ≤ lt → lt ≤ yinj l + m → K1 ≡[T, l] K2. + ∀T. ⬆[l, m] T ≡ U → l ≤ lt → lt ≤ l + m → K1 ≡[T, l] K2. /2 width=11 by llpx_sn_inv_lift_be/ qed-. lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → yinj l + m ≤ lt → K1 ≡[T, lt-m] K2. + ∀T. ⬆[l, m] T ≡ U → l + m ≤ lt → K1 ≡[T, lt-m] K2. /2 width=9 by llpx_sn_inv_lift_ge/ qed-. (* Inversion lemmas on negated lazy quivalence for local environments *******)