From 8910c1dc3fcc1da950d0c71f0f1a0150c5557520 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 18 Feb 2013 21:50:27 +0000 Subject: [PATCH] trace added in a failing invocation of auto :-( --- matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 2.39.2