X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffsle_fqup.ma;h=242c3d52c500cdc7e56f3d5508c9010cfe4a8eeb;hp=34267b7d6f065188a467e6f131e87c33d8449689;hb=076439def28e649ec384fae038ed021dadd5f75c;hpb=d2545ffd201b1aa49887313791386add78fa8603

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
index 34267b7d6..242c3d52c 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
@@ -31,7 +31,7 @@ lemma fsle_shift: ∀L1,L2. |L1| = |L2| →
 #L1 #L2 #H1L #I #T1 #T2 #V
 * #n #m #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
 elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
-lapply (lveq_inv_bind … H2L) -H2L #HL
+lapply (lveq_inv_bind_O … H2L) -H2L #HL
 elim (frees_total L2 V) #g1 #Hg1
 elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 lapply (sor_inv_sle_dx … Hg) #H0g