X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_isi_tl.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_isi_tl.ma;h=4a80d36e42be9a5b6fb173511ab9b026efa77a6f;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=0000000000000000000000000000000000000000;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma new file mode 100644 index 000000000..4a80d36e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma @@ -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 "ground/relocation/gr_tl.ma". +include "ground/relocation/gr_isi.ma". + +(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************) + +(* Properties with tail *****************************************************) + +(*** isid_tl *) +lemma gr_isi_tl (f): 𝐈❪f❫ → 𝐈❪⫱f❫. +#f cases (gr_map_split_tl f) * #H +[ /2 width=3 by gr_isi_inv_push/ +| elim (gr_isi_inv_next … H) -H // +] +qed.