X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_length.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_length.ma;h=7d53c39db77d4572a3c5837cdf73a395ffb5d82c;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=73760857e9e8a0f02cc891ade8f95d61d17b667b;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
index 73760857e..7d53c39db 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_length.ma
@@ -39,7 +39,7 @@ theorem drops_fwd_length_eq1: ∀b1,b2,f,L1,K1. ⇩*[b1,f] L1 ≘ K1 →
   #I2 #K2 #HLK2 #_ #H destruct
   lapply (IH … HLK2 H12) -f >length_bind >length_bind /2 width=1 by/ (**) (* full auto fails *)
 ]
-qed-.  
+qed-.
 
 (* forward lemmas with finite colength assignment ***************************)