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_theq_vector.ma;h=40c508756203c63051a6eae30bf6452bd0c491f7;hp=ec7f35fee7390a466df88ae540033279ed8359e1;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma
index ec7f35fee..40c508756 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_computation/cpxs_theq.ma".
 
 (* Vector form of forward lemmas with head equivalence for terms ************)
 
-lemma cpxs_fwd_sort_vector: ∀h,G,L,s,Vs,X2. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
+lemma cpxs_fwd_sort_vector: ∀h,G,L,s,Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.⋆s ⬈*[h] X2 → ⒶVs.⋆s ⩳ X2.
 #h #G #L #s #Vs elim Vs -Vs /2 width=4 by cpxs_fwd_sort/
 #V #Vs #IHVs #X2 #H
 elim (cpxs_inv_appl1 … H) -H *
@@ -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 →
-                                   ∀Vs,X2. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
-                                   ∨∨ ⒶVs.#i ⩳ X2 | ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
+                                   ∀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
 elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
 #V #Vs #IHVs #X2 #H -K -V1
@@ -62,8 +62,8 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,p,G,L,Vs,V,W,T,X2. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
-                            ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G, L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
+lemma cpxs_fwd_beta_vector: ∀h,p,G,L,Vs,V,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] X2 →
+                            ∨∨ ⒶVs.ⓐV.ⓛ{p}W. T ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] X2.
 #h #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
 #V0 #Vs #IHVs #V #W #T #X2 #H
 elim (cpxs_inv_appl1 … H) -H *
@@ -87,8 +87,8 @@ qed-.
 
 (* Basic_1: was just: pr3_iso_appls_abbr *)
 lemma cpxs_fwd_theta_vector: ∀h,G,L,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.
+                             ∀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/
 #V1b #V2b #V1a #V2a #HV12a #HV12b #p
 generalize in match HV12a; -HV12a
@@ -135,10 +135,10 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,G,L,Vs,W,T,X2. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
+lemma cpxs_fwd_cast_vector: ∀h,G,L,Vs,W,T,X2. ⦃G,L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
                             ∨∨ ⒶVs. ⓝW. T ⩳ X2
-                             | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] X2
-                             | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
+                             | ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2
+                             | ⦃G,L⦄ ⊢ ⒶVs.W ⬈*[h] X2.
 #h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
 #V #Vs #IHVs #W #T #X2 #H
 elim (cpxs_inv_appl1 … H) -H *
@@ -166,8 +166,8 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
-                           ∀Vs,X2. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
+lemma cpxs_fwd_cnx_vector: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
+                           ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.T ⬈*[h] X2 → ⒶVs.T ⩳ X2.
 #h #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
 #V #Vs #IHVs #X2 #H
 elim (cpxs_inv_appl1 … H) -H *