X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;h=de512457b41ca1c304ab8f7c217932d20d79ff85;hb=6386442a6850f86fe24a16871b84961fd2aee47c;hp=7046b8ce95aea63ed81a227d0d01c15646b2ae6f;hpb=f16bf89d854b0c2658d6c622ef5f2bcb8a3cd45a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index 7046b8ce9..de512457b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -64,7 +64,7 @@ lemma frees_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
 | #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
   [ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
     #H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
-    /2 width=3 by sle_refl, ex2_intro/
+    /3 width=3 by sle_refl, ex2_intro/
   | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
     #HL12 #g1 <tls_xn <tl_next_rew #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
     /2 width=3 by ex2_intro/