X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_tps.ma;h=df8a73c5aacad896acc669017083392eded441ad;hb=78d4844bcccb3deb58a3179151c3045298782b18;hp=9c670a8932a1eb7f77ef2fe7af7d26cd234ee993;hpb=6ebf3e5a09012b3349c6020fe692c3b22020684a;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma
index 9c670a893..df8a73c5a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma
@@ -18,9 +18,9 @@ include "basic_2/unfold/ltpss_ldrop.ma".
 
 (* Properties concerning partial substitution on terms **********************)
 
-lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                         ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 →
-                         L1 ⊢ T2 [d2, e2] ▶ U2.
+lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+                         ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+                         L1 ⊢ T2 ▶ [d2, e2] U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
@@ -32,9 +32,9 @@ lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
 ]
 qed.
 
-lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
-                          ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 →
-                          L1 ⊢ T2 [d2, e2] ▶ U2.
+lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+                          ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+                          L1 ⊢ T2 ▶ [d2, e2] U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2