X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcpxs_cpxs.ma;h=c02d0cd069dff45dc740080ad6cfafb9d1659a0f;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=6f8e0ffcb8c5ced0b9b09cf3f7f844bca027cb95;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index 6f8e0ffcb..c02d0cd06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -147,7 +147,7 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2,
   [1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/
   | #H0 destruct /2 width=1 by/
   ]
-| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
+| #G #L #K #T1 #U1 #m #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (m+1))
   #U2 #HTU2 @(ex3_intro … U2)
   [1,3: /2 width=10 by cpxs_lift, fqu_drop/
   | #H0 destruct /3 width=5 by lift_inj/