X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_tpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_tpr.ma;h=43c48d0f2cc756fcefdf99eb9eaacc8fdbbef1e8;hb=cd0870e2572a77bd69bda4b8c403c30b569c58b9;hp=27f09e20a36b7c7d80d305b4b0173bb7dac3ceb6;hpb=37d40349c3c82a62a8cbced18545bfd526ebe7ff;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
index 27f09e20a..43c48d0f2 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/reduction/tpr_lift.ma".
 include "Basic-2/reduction/tpr_tps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
@@ -128,7 +126,7 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
 elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
 elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
 elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
 @ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
 qed.