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

diff --git a/matita/matita/contribs/lambda/terms/relocating_substitution.ma b/matita/matita/contribs/lambda/terms/relocating_substitution.ma
index ebf08b2f7..4f813396f 100644
--- a/matita/matita/contribs/lambda/terms/relocating_substitution.ma
+++ b/matita/matita/contribs/lambda/terms/relocating_substitution.ma
@@ -145,7 +145,7 @@ qed.
 lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
                            ∀l. dsubstable_dx (lstar S … R l).
 #S #R #HR #l #N #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+@(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/
 qed.
 
 lemma star_dsubstable: ∀R. reflexive ? R →