- new extendedd beta-reductum involving native type annotation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx_cix.ma

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 b7a0406cb0a1fa0ab26e1762ce7442b9cb0101fd..7567f9f9c580f3b5b85bc123f493b253dbb91295 100644 (file)
--- 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