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

diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma
index 3fdcef3f2..fb042bdf6 100644
--- 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-.