X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funwind%2Fsstas_aaa.ma;h=6d7cc3c2fb303e52d24c92af9e4cadb534db84ae;hb=603c8b3cdab901c26f63b5fed2c65e49693cc9a3;hp=fbf485841b7ebcebc32847a1941e688be6536cea;hpb=18bc3082b332504f60345245e716b62ae628e3a7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma
index fbf485841..6d7cc3c2f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_aaa.ma
@@ -21,5 +21,5 @@ include "basic_2/unwind/sstas.ma".
 
 lemma sstas_aaa: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
                  ∀A. L ⊢ T ⁝ A → L ⊢ U ⁝ A.
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T // /3 width=6/
+#h #g #L #T #U #H @(sstas_ind_dx … H) -T // /3 width=6/
 qed.