X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_sn.ma;h=0d13a5a3f5a5f697541280d7e20b6580f0b01ced;hb=ba575c0609015580c1419c17b350de19a158e8e3;hp=95eb9efd9f41b2527855ee8b6d6ab67227a03255;hpb=38a7664fd355705596cb63cac87779688790fcb1;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
index 95eb9efd9..0d13a5a3f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma
@@ -200,7 +200,8 @@ lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 →
     lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
   | -Hd21 normalize in Hde12;
     lapply (lt_to_le_to_lt 0 … Hde12) // #He2
-    lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+    lapply (le_plus_to_minus_r … Hde12) -Hde12
+    /3 width=5 by ltpss_sn_tpss2_lt, tpss_weak/ (**) (* /3 width=5/ used to work *)
   ]
 ]
 qed.