- new pointes can point to any subterm

[helm.git] / matita / matita / contribs / lambda / delifting_substitution.ma

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index 79a65396abd7f2e13021d5214823538c3034ac3d..6ad8d252c8114c1e65ce51a63801e08ab060e564 100644 (file)
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -160,5 +160,6 @@ qed.
 
 lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) →
                            ∀l. dsubstable_dx (lstar T … R l).
-#T #R #HR #l #D #M1 #M2 #H elim H -l -M1 -M2 // /3 width=3/
+#T #R #HR #l #D #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
 qed.