λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops_length.ma

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 73760857e9e8a0f02cc891ade8f95d61d17b667b..7d53c39db77d4572a3c5837cdf73a395ffb5d82c 100644 (file)
--- 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 ***************************)