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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index d558b90c0..dac9cd153 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/static/lsubd_da.ma".
 include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_cpes.ma".
+include "basic_2/dynamic/snv_scpes.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
 
@@ -66,11 +66,11 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   | #b #V2 #W #W2 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW #HU
     lapply (da_inv_bind … Hl) -Hl #Hl
-    elim (cpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
+    elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
     elim (snv_fwd_da … HV1) #l1 #Hl1
     elim (snv_fwd_da … HW) #l0 #Hl0
-    lapply (cpds_div … W … 0 … HVW1) /2 width=2 by cprs_cpds/ -W3 #H
-    elim (da_cpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
+    lapply (scpds_div … W … 0 … HVW1) /2 width=2 by cprs_scpds/ -W3 #H
+    elim (da_scpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
     <minus_n_O #H destruct >(plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1
     lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ]
     lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW