X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fpath.ma;h=743ec4c348f12b1985f07b6e9186ca3ba1884876;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=1993d056b1090634d2eec430fd847d5b488c9b74;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma
index 1993d056b..743ec4c34 100644
--- a/matita/matita/contribs/lambda/paths/path.ma
+++ b/matita/matita/contribs/lambda/paths/path.ma
@@ -81,7 +81,7 @@ lemma in_inner_ind: ∀R:predicate path.
                     (∀p. in_inner p → R p → R (dx::p)) →
                     ∀p. in_inner p → R p.
 #R #H1 #H2 #IH #p elim p -p
-[ #H elim (H ?) -H //
+[ #H elim (H …) -H //
 | * #p #IHp // #H
   lapply (in_inner_inv_dx … H) -H /3 width=1/
 ]