X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpm_drops.ma;h=beddc2697d0e9a5277ec643012c1a8048be7cc6a;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=46a1e039d1405f482d6a54f22f777dbbc5968684;hpb=e0f7a5025addf275e40372da3a39b0adacc8106f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
index 46a1e039d..beddc2697 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
@@ -143,9 +143,9 @@ fact cpm_fwd_plus_aux (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
   elim IHU [|*: // ] -IHU #U #HU1 #HU2
   elim IHT [|*: // ] -IHT #T #HT1 #HT2
   /3 width=5 by cpm_cast, ex2_intro/
-| #n #G #K #V #T1 #T2 #V2 #_ #IH #HVT2 #n1 #n2 #H destruct
+| #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct
   elim IH [|*: // ] -IH #T #HT1 #HT2
-  /3 width=6 by cpm_zeta, cpm_bind, ex2_intro/
+  /3 width=3 by cpm_zeta, ex2_intro/
 | #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
   elim IH [|*: // ] -IH #T #HT1 #HT2
   /3 width=3 by cpm_eps, ex2_intro/