- ng_refiner:

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

diff --git a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma
index 558968e254531264fb70a941753a1c517c20699a..2287c6b81053d22ee1fbb618be56964d098eab98 100644 (file)
--- a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma
@@ -37,7 +37,7 @@ qed-.
 lemma l_sreds_fwd_mult: ∀S,R. (∀a,M,N. R a M N → M ↦ N) →
                         ∀l,M1,M2. l_sreds S R l M1 M2 →
                         ♯{M2} ≤ ♯{M1} ^ (2 ^ (|l|)).
-#S #R #HR #l #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 normalize //
+#S #R #HR #l #M1 #M2 #H @(lstar_ind_l … l M1 H) -l -M1 normalize //
 #a #l #M1 #M #HM1 #_ #IHM2
 lapply (HR … HM1) -HR -a #HM1
 lapply (sred_fwd_mult … HM1) #HM1