- degree assignment, static type assignment, iterated static type

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
index a11bb4892f9749cf0b10f133e02f3da220a0d856..2f79d793bbe8c8d05d8719a9d04c7858bc8217f6 100644 (file)
--- 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.