updating the structures for sorts

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpm_tdeq.ma

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 c10cdba20ac48e9842bb8e16f74cc2801965ef25..e3057788cd5018f5a88f98a207ee4ecb7795e72b 100644 (file)
--- 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)