partial commit in the relocation component to move some files ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_weight.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
index 0116254957011dd23e186b98f7f4ca96ad8723e6..d0dc9e7a080f29905924bebb2dafdf51edc38e72 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
@@ -37,7 +37,7 @@ lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
 [ #f #Hf #Hnf elim Hnf -Hnf /2 width=1 by/
 | /3 width=3 by drops_fwd_lw, le_to_lt_to_lt/
 | #I #L1 #L2 #V1 #V2 #f #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I
-  >(lifts_fwd_tw … HV21) -V2 /5 width=1 by isid_push, monotonic_lt_plus_l/
+  >(lifts_fwd_tw … HV21) -V2 /5 width=3 by isid_push, monotonic_lt_plus_l/
 ]
 qed-.