- ng_refiner:

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

diff --git a/matita/matita/contribs/lambda/terms/relocation.ma b/matita/matita/contribs/lambda/terms/relocation.ma
index 62da59661cd708002a90b095b555e91796ae2f11..15c7fde8c78ee6c04cdc4f642eed2f3bc2d4e046 100644 (file)
--- a/matita/matita/contribs/lambda/terms/relocation.ma
+++ b/matita/matita/contribs/lambda/terms/relocation.ma
@@ -244,13 +244,13 @@ qed-.
 lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
                       ∀l. liftable (lstar S … R l).
 #S #R #HR #l #h #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 lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
                            ∀l. deliftable_sn (lstar S … R l).
 #S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+@(lstar_ind_l … l N1 H) -l -N1 /2 width=3/
 #a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
 elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
 elim (IHN2 … HMN) -N /3 width=3/