X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fbackground%2Fpreamble.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda%2Fbackground%2Fpreamble.ma;h=6455bfcf41bdcb4920663e968a4d300a70fa1779;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=769ffa5a366838ff9dd5660e3440d72f1a540cdd;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma
index 769ffa5a3..6455bfcf4 100644
--- a/matita/matita/contribs/lambda/background/preamble.ma
+++ b/matita/matita/contribs/lambda/background/preamble.ma
@@ -122,7 +122,7 @@ qed.
 (* Note: this cannot be in lib because of the missing xoa quantifier *)
 lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
                      ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
-#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1
 [ #H elim (lt_refl_false … H)
 | #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
 ]