some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
index 3c65cbd7c6e204f3c1062811ba6e2531039331b2..99d2b7e129f0e71ed06c5bbc8fbee71866297269 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/cnv.ma".
 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
 
 definition ntas (a) (h) (n) (G) (L): relation term ≝ λT,U.
-           ∃∃U0. ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[n,h] U0.
+           ∃∃U0. ⦃G,L⦄ ⊢ U ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[n,h] U0.
 
 interpretation "iterated native type assignment (term)"
    'Colon a h n G L T U = (ntas a h n G L T U).