- predefined_virtuals: nwe characters

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / ltpss_sn.ma

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 95eb9efd9f41b2527855ee8b6d6ab67227a03255..0d13a5a3f5a5f697541280d7e20b6580f0b01ced 100644 (file)
--- 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.