X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind1%2Funwind_structure_depth.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind1%2Funwind_structure_depth.etc;h=0000000000000000000000000000000000000000;hb=084fe5719d41ce13be068050fbade488d4a183ee;hp=df3423e164aa3107f8d5c2407ccc6581b315e20b;hpb=61bc42e04598a9f5e489c3867af72e700c7fda04;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc deleted file mode 100644 index df3423e16..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "delayed_updating/unwind1/unwind.ma". -include "delayed_updating/syntax/path_structure.ma". -include "delayed_updating/syntax/path_depth.ma". -include "ground/arith/nat_pred_succ.ma". - -(* UNWIND FOR PATH *********************************************************) - -(* Basic constructions with structure and depth ****************************) - -lemma unwind_rmap_structure (p) (f): - (⫯*[♭p]f) = ▼[⊗p]f. -#p elim p -p // -* [ #n ] #p #IH #f // -[