X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_labels.ma;h=d139018f7218d7f4150775c75931a285410fbc8c;hb=41a54a797af98d2867d4bf979d424283fb44a1fc;hp=b1ddacd6f4b873a075acf43b54af341bb9b1136a;hpb=dfcad1c1a698bac1b7fb6a5f59393b28f45182af;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma index b1ddacd6f..d139018f7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma @@ -16,7 +16,7 @@ include "delayed_updating/unwind/unwind2_rmap.ma". include "delayed_updating/syntax/path_labels.ma". include "ground/relocation/tr_pushs.ma". -(* UNWIND MAP FOR PATH ******************************************************) +(* TAILED UNWIND FOR RELOCATION MAP *****************************************) (* Constructions with labels ************************************************) @@ -24,5 +24,5 @@ lemma unwind2_rmap_labels_L (f) (n): (⫯*[n]f) = ▶[f](𝗟∗∗n). #f #n @(nat_ind_succ … n) -n // #n #IH -