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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 66ddc0d99..84bbfeda9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -35,7 +35,7 @@ interpretation "extended native type assignment (term)"
 
 (* Basic_1: was by definition: ty3_sort *)
 (* Basic_2A1: was by definition: nta_sort ntaa_sort *)
-lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(next h s).
+lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(⫯[h]s).
 #a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
 qed.