- parallel substitution reaxiomatized

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / tps.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
index af450e34df23c26043d8dbf39657fefc65fac4fe..7d89243d5d6583091bb696fd63e8e6f0f1c5c7b0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.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 @{ 'PSubst $L $T1 $d $e $T2 }.
+
 include "basic_2/substitution/ldrop_append.ma".
 
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
@@ -91,8 +95,8 @@ lemma tps_weak_top: ∀L,T1,T2,d,e.
 ]
 qed.
 
-lemma tps_weak_all: ∀L,T1,T2,d,e.
-                    L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
+lemma tps_weak_full: ∀L,T1,T2,d,e.
+                     L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2.
 #L #T1 #T2 #d #e #HT12
 lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
 lapply (tps_weak_top … HT12) //