X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Fhead%2Funwind2_rmap_labels.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Fhead%2Funwind2_rmap_labels.etc;h=d139018f7218d7f4150775c75931a285410fbc8c;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hp=0000000000000000000000000000000000000000;hpb=41a54a797af98d2867d4bf979d424283fb44a1fc;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc new file mode 100644 index 000000000..d139018f7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/unwind2_rmap.ma". +include "delayed_updating/syntax/path_labels.ma". +include "ground/relocation/tr_pushs.ma". + +(* TAILED UNWIND FOR RELOCATION MAP *****************************************) + +(* Constructions with labels ************************************************) + +lemma unwind2_rmap_labels_L (f) (n): + (⫯*[n]f) = ▶[f](𝗟∗∗n). +#f #n @(nat_ind_succ … n) -n // +#n #IH +