X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_toeq_vector.ma;h=20702a3546b1c91bc2980ad8ea02bf19ad415d8d;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=bbd7c5c9def31a611380d507993b9214a5f8bcb4;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
index bbd7c5c9d..20702a354 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
@@ -37,8 +37,8 @@ qed-.
 
 (* Basic_2A1: was: cpxs_fwd_delta_vector *)
 lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
-      ∀V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
-      ∀V2. ⬆*[↑i] V1 ≘ V2 →
+      ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
+      ∀V2. ⇧*[↑i] V1 ≘ V2 →
       ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
       ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
 #h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
@@ -90,7 +90,7 @@ qed-.
 
 (* Basic_1: was just: pr3_iso_appls_abbr *)
 lemma cpxs_fwd_theta_vector (h) (G) (L):
-      ∀V1b,V2b. ⬆*[1] V1b ≘ V2b →
+      ∀V1b,V2b. ⇧*[1] V1b ≘ V2b →
       ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
       ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
 #h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/