- relation between native type and atomic arity proced

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / nta_nta.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
index b36725d92ffc54a1c24c275c5bb21730304db7ab..05eb6c55df0ae58fd6ae7a34f9431b60b0c81c26 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
@@ -37,10 +37,10 @@ theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T
   elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
-  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H
-  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #T #U1 #_ #_ #X #H
   elim (nta_inv_cast1 … H) -H //