X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fdelift_alt.ma;h=75ce099571c1a3631b2d1ed2064511902fbec664;hb=fba384e357ed3c8781fc018c2c16f2b40df144af;hp=6828b50b7ae8db4fd1dacc4b97d0c89a616fc2dd;hpb=38c81062ae1aedf89d426d5dcd9a27824c4b0fb0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
index 6828b50b7..75ce09957 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma
@@ -82,7 +82,7 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
                       (∀L,d,e,i. i < d → 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 ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
-                       ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+                       ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
                       ) →
                       (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
                       (∀L,d,e,p. R d e L (§p) (§p)) →