milestone uupdate in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma
deleted file mode 100644 (file)
index 320ec67..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma
+++ /dev/null
@@ -1,8 +0,0 @@
-(*
-(* Advanced forvard lemmas **************************************************)
-
-lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
-                     ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
-/2 width=3/ qed-.
-
-*)