- the relocation properties of cpr are closed!

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / tpss_ltps.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
index 1f4a2de3e3bb1a18be75f4b47e14b928d66fcf2b..abaf3f7c0df318a5c376bf7740ea847101a7da65 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
@@ -66,8 +66,8 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
 #L1 #T2 #U2 #d #e * -L1 T2 U2 d e
 [ //
 | #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct -Y1 X2;
-  lapply (drop_fwd_lw … HLK1) normalize #H1
-  elim (ltps_drop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0
+  lapply (ldrop_fwd_lw … HLK1) normalize #H1
+  elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0
   elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
   lapply (tps_fwd_tw … HV01) #H2
   lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H