X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx_drops.ma;h=fe9afa3a88baf5ee27e8728fae0b4ff0d46eb2b0;hb=18d7afd216aee6c815eac30982d8ad4fa4521070;hp=98c2b491fa392555ab26a43960208a8c2c05c73c;hpb=f694e3336cbdabdeefd86f85d827edfd26bf3464;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
index 98c2b491f..fe9afa3a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
@@ -60,7 +60,7 @@ qed-.
 (* Inversion lemmas with generic slicing for local environments *************)
 
 (* Basic_2A1: includes: cpx_inv_lift1 *)
-lemma cpx_inv_lift1: ∀h,G. d_deliftable2_sn (cpx h G).
+lemma cpx_inv_lifts: ∀h,G. d_deliftable2_sn (cpx h G).
 #h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
 elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
 /3 width=4 by ex2_intro, ex_intro/