update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / etc / unwind2 / unwind_etc.etc

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc
deleted file mode 100644 (file)
index a9e563d..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc
+++ /dev/null
@@ -1,10 +0,0 @@
-include "delayed_updating/unwind2/unwind_depth.ma".
-include "ground/relocation/tr_uni_compose.ma".
-
-lemma pippo (q) (p): 
-      ▼[p]𝐢 ≗ ⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢.
-#q @(list_ind_rcons … q) -q //
-#q * [ #n ] #IH #p //
-<depth_d_dx >list_cons_shift <list_append_assoc
-<unwind_rmap_d_dx
-check tr_tls_compose_uni_sn
\ No newline at end of file