- ng_refiner:

[helm.git] / matita / matita / contribs / lambda / terms / sequential_computation.ma

diff --git a/matita/matita/contribs/lambda/terms/sequential_computation.ma b/matita/matita/contribs/lambda/terms/sequential_computation.ma
index 2fc5afd5a7c8bc2f28a7d1754fb2c758e8045268..b248e6027a399f6b8f5544da77371425a0444121 100644 (file)
--- a/matita/matita/contribs/lambda/terms/sequential_computation.ma
+++ b/matita/matita/contribs/lambda/terms/sequential_computation.ma
@@ -78,7 +78,7 @@ lemma sreds_compatible_beta: ∀B1,B2. B1 ↦* B2 → ∀A1,A2. A1 ↦* A2 →
 qed.
 
 theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2.
-#M1 #M2 #H @(star_ind_l ??????? H) -M1 //
+#M1 #M2 #H @(star_ind_l … M1 H) -M1 //
 #M1 #M #HM1 #_ #IHM2
 @(preds_step_sn … IHM2) -M2 /2 width=2/
 qed.