X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs_drops.ma;h=b39c11f95354872059a3cd9cab12097f76c18dac;hb=6555775aa5268dec0d9ae4579412b659cacdc964;hp=9875361f7bd180b359d379de90be8310b29490ff;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 9875361f7..b39c11f95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -37,13 +37,13 @@ definition dropable_dx: predicate (relation3 lenv term term) ≝
 (* Properties with generic slicing for local environments *******************)
 
 (* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *)
-lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
-                                d_liftable2 R → dedropable_sn R.
+lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) →
+                                   d_liftable2_sn R → dedropable_sn R.
 #R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU
 elim (frees_total L1 U) #f2 #Hf2
 lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
-elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
-/3 width=6 by cfull_lift, ex3_intro, ex2_intro/
+elim (lexs_liftable_co_dedropable_sn … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
+/3 width=6 by cfull_lift_sn, ex3_intro, ex2_intro/
 qed-.
 
 (* Inversion lemmas with generic slicing for local environments *************)