From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 18 Feb 2013 21:50:27 +0000 (+0000)
Subject: trace added in a failing invocation of auto :-(
X-Git-Tag: make_still_working~1250
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8910c1dc3fcc1da950d0c71f0f1a0150c5557520;p=helm.git

trace added in a failing invocation of auto :-(
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
index c504e4edc..93e63853f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma
@@ -48,7 +48,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U.
-/3 width=2/ qed.
+/3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *)
 
 lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g,l+1] U2 →
                     ⦃h, L⦄ ⊢ T1 •*[g] U2.