- relation between native type and atomic arity proced

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / tpss_alt.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
index 725dc57f17a2f92234bc5697818e07f258fefce1..30b7e80ac4ce1f22a4b4dbceeda3569d16f21a8a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma
@@ -35,24 +35,24 @@ interpretation "parallel unfold (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 →
-                        ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶▶* T2.
+lemma tpssa_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
+                         ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
 qed.
 
-lemma tpssa_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶▶* T.
+lemma tpssa_refl: ∀T,L,d,e. L ⊢ T ▶▶* [d, e] T.
 #T elim T -T //
 #I elim I -I /2 width=1/
 qed.
 
-lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T →
-                       ∀T2. L ⊢ T [d, e] ▶ T2 → L ⊢ T1 [d, e] ▶▶* T2.
+lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T →
+                       ∀T2. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
 #L #T1 #T #d #e #H elim H -L -T1 -T -d -e
 [ #L #I #d #e #X #H
   elim (tps_inv_atom1 … H) -H // * /2 width=6/
@@ -62,40 +62,40 @@ lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T →
   elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
 | #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
-  lapply (tps_lsubs_conf … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+  lapply (tps_lsubs_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
   lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
   lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
-  lapply (tpssa_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (tpssa_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
 | #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
 ]
 qed.
 
-lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶▶* T2.
+lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
 #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶▶* T2 → L ⊢ T1 [d, e] ▶* T2.
+lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
 qed-. 
 
 lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
                     (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
                     (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
-                     ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ▶* V2 →
+                     ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →
                      ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
                     ) →
-                    (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
-                     L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ▶* T2 → R d e L V1 V2 →
+                    (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
+                     L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 →
                      R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
                     ) →
-                    (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
-                     L⊢ T1 [d, e] ▶* T2 → R d e L V1 V2 →
+                    (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
+                     L ⊢ T1 ▶* [d, e] T2 → R d e L V1 V2 →
                      R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
                     ) →
-                    ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ▶* T2 → R d e L T1 T2.
+                    ∀d,e,L,T1,T2. L ⊢ T1 ▶* [d, e] T2 → R d e L T1 T2.
 #R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e
 // /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/
 qed-.