X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_ind.ma;h=89565cde7a4aef6f09bdc69b42b82837d6f6bca2;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=4de1ae8019b368e26b172f24c38685620de5978d;hpb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 4de1ae801..89565cde7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -22,7 +22,7 @@ include "basic_2/dynamic/nta_preserve.ma".
 (* Advanced eliminators *****************************************************)
 
 lemma nta_ind_rest_cnv (h) (Q:relation4 …):
-      (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+      (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
         ⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
@@ -71,7 +71,7 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
   /4 width=5 by nta_bind_cnv/
 | #V #T #HG #HL #HT #X #H destruct
   elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
-  /4 width=9 by nta_appl/
+  /4 width=9 by nta_appl, ylt_inj/
 | #U #T #HG #HL #HT #X #H destruct
   elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
   /4 width=4 by nta_cast/
@@ -79,7 +79,7 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
 qed-.
 
 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
-      (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+      (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
         ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
@@ -144,7 +144,7 @@ lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
 qed-.
 
 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
-      (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+      (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
         ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
@@ -179,5 +179,5 @@ lemma nta_ind_ext_cnv (h) (Q:relation4 …):
 lapply (nta_fwd_cnv_dx … HTU) #H
 elim (cnv_inv_bind … H) -H #_ #HU
 elim (cnv_nta_sn … HU) -HU #X #HUX
-/4 width=2 by nta_beta, nta_fwd_cnv_sn/
+/4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/
 qed-.