update in lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / fsle_fqup.ma

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 34267b7d6f065188a467e6f131e87c33d8449689..242c3d52c500cdc7e56f3d5508c9010cfe4a8eeb 100644 (file)
--- 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