X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss_alt.ma;h=f7670eaa807e5e17429c5bbd2dd654e41adf5438;hb=eb4b3b1b307fc392c36f0be253e6a111553259bc;hp=8f77dd0d0d8e3115a3dd805428e1b1d76ac5ed0e;hpb=08cb57944c0df08611d4f35d286e46c0d13e4813;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
index 8f77dd0d0..f7670eaa8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -12,6 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+
 include "basic_2/unfold/tpss_lift.ma".
 
 (* PARALLEL UNFOLD ON TERMS *************************************************)
@@ -35,12 +39,12 @@ interpretation "parallel unfold (term) alternative"
 
 (* Basic properties *********************************************************)
 
-lemma tpssa_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
-                         ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
+lemma tpssa_lsubr_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_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -62,10 +66,10 @@ 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 #a #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_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+  lapply (tps_lsubr_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_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+  lapply (tpssa_lsubr_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/
 ]