- ng_refiner:

[helm.git] / matita / matita / contribs / lambda / paths / path.ma

diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma
index 1993d056b1090634d2eec430fd847d5b488c9b74..743ec4c348f12b1985f07b6e9186ca3ba1884876 100644 (file)
--- 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/
 ]