X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fltpr_aaa.ma;h=ef63ad095d6468eadd660da10e5ce28a493c37ce;hb=cc21d0caa6229b7d1a905f9b62de2af4f40cc863;hp=1a551cec290830515a4dddb2eaf82bd8fc9dabf5;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
index 1a551cec2..ef63ad095 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/aaa_ltpss.ma".
+include "basic_2/static/aaa_ltpss_dx.ma".
 include "basic_2/static/lsuba_aaa.ma".
 include "basic_2/reducibility/ltpr_ldrop.ma".
 
@@ -29,7 +29,7 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T
 | #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct
   >(tpr_inv_atom1 … H) -T2
   lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1
-  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
   lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
 | #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct