X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Flleq_drop.ma;h=a15862996d7cfe15e6776bade1e99fb5ca72c8c6;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=5bf3ddfc630b1f01e036447ce22633aa35f00ab3;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq_drop.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq_drop.ma
index 5bf3ddfc6..a15862996 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq_drop.ma
@@ -138,7 +138,7 @@ lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
 (* Inversion lemmas on negated lazy quivalence for local environments *******)
 
 lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) →
-                      (L1 ≡[V, l] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → ⊥).
+                      (L1 ≡[V, l] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, ↑l] L2.ⓑ{I}V → ⊥).
 /3 width=2 by nllpx_sn_inv_bind, eq_term_dec/ qed-.
 
 lemma nlleq_inv_flat: ∀I,L1,L2,V,T,l. (L1 ≡[ⓕ{I}V.T, l] L2 → ⊥) →