X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Fheight%2Fpath_height_labels.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Fheight%2Fpath_height_labels.etc;h=fb55c3606ac585ab1893242688812096203e8e7a;hb=df1bcd1387439133c0c33f597a5f8b2331c07772;hp=0000000000000000000000000000000000000000;hpb=119da3f9ce130f7c4e8b23fcc491d221472ad657;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height_labels.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height_labels.etc new file mode 100644 index 000000000..fb55c3606 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height_labels.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/path_height.ma". +include "delayed_updating/syntax/path_labels.ma". + +(* HEIGHT FOR PATH **********************************************************) + +(* Constructions with labels ************************************************) + +lemma height_labels_L (n): + (𝟎) = ♯(𝗟∗∗n). +#n @(nat_ind_succ … n) -n // +#n #IH