X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Ftpss_ltps.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Ftpss_ltps.ma;h=abaf3f7c0df318a5c376bf7740ea847101a7da65;hb=035e3f52f8da3cb3cdb493aa20568ad673cc2cf5;hp=1f4a2de3e3bb1a18be75f4b47e14b928d66fcf2b;hpb=83aea9a1662de32505512d6296921ebfffcfc53d;p=helm.git

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 1f4a2de3e..abaf3f7c0 100644
--- 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