X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss_alt.ma;h=46e064ca9fab22d5549076b3f2b5807d6986a7c4;hb=fba384e357ed3c8781fc018c2c16f2b40df144af;hp=ae1dcf624a02809aa5942830e55913312feabe22;hpb=38c81062ae1aedf89d426d5dcd9a27824c4b0fb0;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 ae1dcf624..46e064ca9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
@@ -81,11 +81,11 @@ lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [
 #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.
+lemma tpss_ind_alt: ∀R:nat→nat→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 + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+                     ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
                     ) →
                     (∀L,a,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 →