X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_teqo_vector.ma;h=b3236af74387e02b43290bb74bd1345749085450;hp=4962015793e08ee8757a34cdf78d35ab37338ade;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
index 496201579..b3236af74 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_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/