X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_aaa.ma;h=d663b30097e6dff24c7fbbf407ab2c97e6dbd670;hb=5a35a42e23b2f343f0241eeb6648bf05f31720db;hp=d947c016fc66afc3276cc1762f1990a513e86490;hpb=8c0dca9afa666cb4c993fef8e4870388b97c5975;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
index d947c016f..d663b3009 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/static/da_aaa.ma".
-include "basic_2/computation/csx_aaa.ma".
 include "basic_2/computation/scpds_aaa.ma".
 include "basic_2/dynamic/snv.ma".
 
@@ -38,10 +37,6 @@ lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄
 ]
 qed-.
 
-lemma snv_fwd_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_csx/
-qed-.
-
 (* Advanced forward lemmas **************************************************)
 
 lemma snv_fwd_da: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l.