- ng_refiner:

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

diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma
index 3fdcef3f26a6c845ea3e400aff5ef68f90db067d..fb042bdf65b70b6b18b9417e1016c7bd4e4805b9 100644 (file)
--- a/matita/matita/contribs/lambda/paths/trace.ma
+++ b/matita/matita/contribs/lambda/paths/trace.ma
@@ -69,5 +69,5 @@ lemma is_inner_append: ∀r. is_inner r → ∀s. is_inner s → is_inner (r@s).
 qed.
 
 lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s.
-* // #p #s * #H1p #_ * #H2p #_ elim (H2p ?) -H2p //
+* // #p #s * #H1p #_ * #H2p #_ elim (H2p …) -H2p //
 qed-.