update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / ltpr_ltpss_dx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
index cee1cb49e53e08d62e6f402cca34cdde9c94d345..00730b732948937d8e97610bbaa537e123173ed8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/ltpr_tpss.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
 
@@ -27,10 +27,10 @@ lemma ltpr_ltpss_dx_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 
 | #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
   elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
-  elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+  elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
 | #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
   elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
   elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
-  elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+  elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/
 ]
 qed.