X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fterms%2Flabeled_sequential_computation.ma;h=2287c6b81053d22ee1fbb618be56964d098eab98;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=558968e254531264fb70a941753a1c517c20699a;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma
index 558968e25..2287c6b81 100644
--- 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