- grafiteParser: we added the comand "defined" as a presentational

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_aaa.ma

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 d947c016fc66afc3276cc1762f1990a513e86490..d663b30097e6dff24c7fbbf407ab2c97e6dbd670 100644 (file)
--- 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.