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=ec7f35fee7390a466df88ae540033279ed8359e1;hp=8c03262064abb5b3cda28727b778ae581fe9a981;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

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 8c0326206..ec7f35fee 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,90 +20,82 @@ include "basic_2/rt_computation/cpxs_theq.ma".
 
 (* Vector form of forward lemmas with head equivalence for terms ************)
 
-lemma cpxs_fwd_sort_vector: ∀h,o,G,L,s,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆s ⬈*[h] U →
-                            ⒶVs.⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h s) ⬈*[h] U.
-#h #o #G #L #s #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
-#V #Vs #IHVs #U #H
+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 *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair/
 | #p #W1 #T1 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (theq_inv_applv_bind_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV.ⓛ{p}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
-  ]
+  lapply (IHVs … HT1) -IHVs -HT1 #HT1
+  elim (theq_inv_applv_bind_simple … HT1) //
 | #p #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
-  elim (IHVs … HT1) -IHVs -HT1 #HT1
-  [ elim (theq_inv_applv_bind_simple … HT1) //
-  | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
-    @(cpxs_strap1 … (ⓐV1.ⓓ{p}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
-  ]
+  lapply (IHVs … HT1) -IHVs -HT1 #HT1
+  elim (theq_inv_applv_bind_simple … HT1) //
 ]
 qed-.
 
 (* Basic_2A1: was: cpxs_fwd_delta_vector *)
-lemma cpxs_fwd_delta_drops_vector: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+lemma cpxs_fwd_delta_drops_vector: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
                                    ∀V2. ⬆*[↑i] V1 ≘ V2 →
-                                   ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ⬈*[h] U →
-                                   ⒶVs.#i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ⬈*[h] U.
-#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta_drops/
-#V #Vs #IHVs #U #H -K -V1
+                                   ∀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
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
 | #q #W0 #T0 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
   [ elim (theq_inv_applv_bind_simple … HT0) //
   | @or_intror -i (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /3 width=1 by cpxs_flat_dx, cpx_beta/
   ]
 | #q #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
   [ elim (theq_inv_applv_bind_simple … HT0) //
   | @or_intror -i (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV0.ⓓ{q}V3.T0)) /3 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,o,p,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{p}W.T ⬈*[h] U →
-                            ⒶVs.ⓐV.ⓛ{p}W. T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{p}ⓝW.V.T ⬈*[h] U.
-#h #o #p #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #U #H
+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 *
 [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
 | #q #W1 #T1 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
   [ elim (theq_inv_applv_bind_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV0.ⓛ{q}W1.T1)) /3 width=1 by cpxs_flat_dx, cpx_beta/
   ]
 | #q #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
   elim (IHVs … HT1) -IHVs -HT1 #HT1
   [ elim (theq_inv_applv_bind_simple … HT1) //
   | @or_intror (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV1.ⓓ{q}V3.T1)) /3 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector: ∀h,o,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
-                             ∀p,V,T,U. ⦃G, L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] U →
-                             ⒶV1b.ⓓ{p}V.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] U.
-#h #o #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/
+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.
+#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
 generalize in match V2a; -V2a
 generalize in match V1a; -V1a
 elim HV12b -V1b -V2b /2 width=1 by cpxs_fwd_theta/
-#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #U #H
+#V1b #V2b #V1b #V2b #HV12b #_ #IHV12b #V1a #V2a #HV12a #V #T #X2 #H
 elim (cpxs_inv_appl1 … H) -H *
 [ -IHV12b -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or_introl/
 | #q #W0 #T0 #HT0 #HU
@@ -111,7 +103,7 @@ elim (cpxs_inv_appl1 … H) -H *
   [ -HV12a -HV12b -HU
     elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct
   | @or_intror -V1b (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
     [ -HV12a #V1 #T1 #_ #_ #H destruct
     | -V1b #X #HT1 #H #H0 destruct
@@ -126,7 +118,7 @@ elim (cpxs_inv_appl1 … H) -H *
   [ -HV12a -HV10a -HV0a -HU
     elim (theq_inv_pair1 … HT0) #V1 #T1 #H destruct
   | @or_intror -V1b -V1b (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     elim (cpxs_inv_abbr1_dx … HT0) -HT0 *
     [ #V1 #T1 #HV1 #HT1 #H destruct
       lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
@@ -143,41 +135,41 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,o,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ⬈*[h] U →
-                            ∨∨ ⒶVs. ⓝW. T ⩳[h, o] U
-                             | ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U
-                             | ⦃G, L⦄ ⊢ ⒶVs.W ⬈*[h] U.
-#h #o #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
-#V #Vs #IHVs #W #T #U #H
+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.
+#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 *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair, or3_intro0/
 | #q #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
   [ elim (theq_inv_applv_bind_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
   | @or3_intro2 -T (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV.ⓛ{q}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
   ]
 | #q #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
   elim (IHVs … HT0) -IHVs -HT0 #HT0
   [ elim (theq_inv_applv_bind_simple … HT0) //
   | @or3_intro1 -W (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
   | @or3_intro2 -T (**) (* explicit constructor *)
-    @(cpxs_trans … HU) -U
+    @(cpxs_trans … HU) -X2
     @(cpxs_strap1 … (ⓐV0.ⓓ{q}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
   ]
 ]
 qed-.
 
 (* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
-                           ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ⬈*[h] U → ⒶVs.T ⩳[h, o] U.
-#h #o #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 #U #H
+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 *
 [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by theq_pair/
 | #p #W0 #T0 #HT0 #HU