X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Ftpss.ma;h=dd2c219ff94ab8ece693e793359d85d599c08082;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=d0f96418633de827746c3655a9f7745c76898f23;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
index d0f964186..dd2c219ff 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -155,7 +155,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2].
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
 #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT1
 lapply (tps_fwd_tw … HT2) -HT2 #HT2