X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsx_csx.ma;h=843bea88b58c72dffd01eebb89d564731c6da57a;hb=5d669f492522b055f76c627eb89da97d0be05c2a;hp=7dc0b2a856388864772843961098f80ed00c52c1;hpb=c69a33bba2ae2f37953737940fb45149136cf054;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
index 7dc0b2a85..843bea88b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
@@ -48,7 +48,7 @@ theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⬊*[
 [ #i #HG #HL #HT #H #d destruct
   elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
   elim (ylt_split i d) /2 width=1 by lsx_lref_skip/
-  #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
+  #Hdi #Hi elim (ldrop_O1_lt (Ⓕ) … Hi) -Hi
   #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
   /4 width=6 by lsx_lref_be, fqup_lref/
 | #a #I #V #T #HG #HL #HT #H #d destruct