X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcpxs.ma;h=2f79d793bbe8c8d05d8719a9d04c7858bc8217f6;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=a11bb4892f9749cf0b10f133e02f3da220a0d856;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index a11bb4892..2f79d793b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predstar_6.ma".
-include "basic_2/unfold/sstas.ma".
 include "basic_2/reduction/cnx.ma".
 include "basic_2/computation/cprs.ma".
 
@@ -61,11 +60,6 @@ lemma lsubr_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) lsubr.
 /3 width=5 by lsubr_cpx_trans, TC_lsub_trans/
 qed-.
 
-lemma sstas_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •* [h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2 //
-/3 width=4 by cpxs_strap1, ssta_cpx/
-qed.
-
 lemma cprs_cpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
 #h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
 qed.