X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpm_tdeq.ma;h=e3057788cd5018f5a88f98a207ee4ecb7795e72b;hp=c10cdba20ac48e9842bb8e16f74cc2801965ef25;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hpb=f308429a0fde273605a2330efc63268b4ac36c99

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
index c10cdba20..e3057788c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
@@ -128,7 +128,7 @@ qed-.
 
 lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …):
                    (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) →
-                   (∀L,s. n = 1 → Q L (⋆s) (⋆(next h s))) →
+                   (∀L,s. n = 1 → Q L (⋆s) (⋆(⫯[h]s))) →
                    (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T1![a,h] →
                     ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
                     Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)