- full commit for the transtive closure of ltpss!

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / ltpr_aaa.ma

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 1a551cec290830515a4dddb2eaf82bd8fc9dabf5..ef63ad095d6468eadd660da10e5ce28a493c37ce 100644 (file)
--- 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