X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpx_cix.ma;h=7567f9f9c580f3b5b85bc123f493b253dbb91295;hb=f62eeb3c7824564ccbe4fff6e75ddee46ca39cc0;hp=b7a0406cb0a1fa0ab26e1762ce7442b9cb0101fd;hpb=ef49e0e7f5f298c299afdd3cbfdc2404ecb93879;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
index b7a0406cb..7567f9f9c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
@@ -40,7 +40,9 @@ lemma cpx_fwd_cix: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ 
   elim (cix_inv_ri2 … H) /2 width=1/
 | #L #V1 #T1 #T2 #_ #_ #H
   elim (cix_inv_ri2 … H) /2 width=1/
-| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+| #L #V1 #V2 #T #_ #_ #H
+  elim (cix_inv_ri2 … H) /2 width=1/
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
   elim (cix_inv_appl … H) -H #_ #_ #H
   elim (simple_inv_bind … H)
 | #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H