notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lcosx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
index 79e147a750709cad000fdfc3e9153f84fcf2b948..03187e34c8d49604d649b6b09165ed1bb9e60bcf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
@@ -35,7 +35,7 @@ lemma lcosx_O: ∀h,g,G,L. G ⊢ ~⬊*[h, g, 0] L.
 qed.
 
 lemma lcosx_drop_trans_lt: ∀h,g,G,L,d. G ⊢ ~⬊*[h, g, d] L →
-                            â\88\80I,K,V,i. â\87©[i] L ≡ K.ⓑ{I}V → i < d →
+                            â\88\80I,K,V,i. â¬\87[i] L ≡ K.ⓑ{I}V → i < d →
                             G ⊢ ~⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⬊*[h, g, V, ⫰(d-i)] K.
 #h #g #G #L #d #H elim H -L -d
 [ #d #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct