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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
index b1d0f1116..2991481d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
@@ -56,8 +56,8 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
-                      ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
+                      ∀V2. ⬆[0, i + 1] V1 ≡ V2 →
                       ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
                       #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
 #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
@@ -68,7 +68,7 @@ lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
 qed-.
 
 lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
-                      ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
+                      ∀V2. ⬆[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
                       ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
 #h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
 elim (cpxs_inv_appl1 … H) -H *