milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / multiple / lleq_drop.ma
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 5bf3ddfc630b1f01e036447ce22633aa35f00ab3..a15862996d7cfe15e6776bade1e99fb5ca72c8c6 100644 (file)
--- 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 â\89¡[V, l] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93\91{I}V â\89¡[T, â«¯l] L2.ⓑ{I}V → ⊥).
+                      (L1 â\89¡[V, l] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93\91{I}V â\89¡[T, â\86\91l] 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 → ⊥) →