X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flcosx.ma;h=03187e34c8d49604d649b6b09165ed1bb9e60bcf;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=79e147a750709cad000fdfc3e9153f84fcf2b948;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
index 79e147a75..03187e34c 100644
--- 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 →
-                            ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d →
+                            ∀I,K,V,i. ⬇[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