X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lstas_lpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lstas_lpr.ma;h=388cf2ba47388182d7f2d8c73302daac3e2818f1;hb=5902d6da146ca78b0ed5d062e3968f52868147c5;hp=a974f248f1bc0563810f427bd95f0eb094624ce3;hpb=ddd6cb6f4514d9ca97f857cafa218c170222f5aa;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
index a974f248f..388cf2ba4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 include "basic_2/dynamic/lsubsv_lstas.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -86,13 +86,13 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
     lapply (da_inv_bind … Hl1) -Hl1 #Hl1
     elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
-    elim (cpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
+    elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
     elim (snv_fwd_da … HW2) #l0 #HW2l
-    lapply (cpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_cpds/ -W0 #H21
+    lapply (scpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_scpds/ -W0 #H21
     elim (snv_fwd_da … HV1) #l #HV1l
-    elim (da_cpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
+    elim (da_scpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
     <minus_n_O #H0 destruct >(plus_minus_m_m l 1) in HV1l; // -H #HV1l
-    lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
+    lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
     lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
     lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
     lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l
@@ -106,8 +106,8 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
       /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
     | -U3
       @(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/
-      @hsnv_cast [1,2: // ] #l0 #Hl0
-      lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
+      @shnv_cast [1,2: // ] #l0 #Hl0
+      lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32
       /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
     | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
     ]