updating the structures for sorts

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
index 100d6317b9a5e543c85996b11be8070924228c30..d4aec09f3609bb23b6cdfc747c360521d63260bb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
@@ -45,7 +45,7 @@ qed-.
 (* Basic_2A1: was: nta_inv_sort1 *)
 lemma nta_inv_sort_sn (a) (h) (G) (L) (X2):
       ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 →
-      ∧∧ ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
+      ∧∧ ⦃G,L⦄ ⊢ ⋆(⫯[h]s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
 #a #h #G #L #X2 #s #H
 elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H
 lapply (cpms_inv_sort1 … H) -H #H destruct