X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_id.ma;h=28eee66dc512a83cc3165c1e4ce84d72a9366086;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hp=8787ecbb998ce72ac70bafa441644659be98980e;hpb=3729defa81f91b5f1259d628299bce9dbc5bfb7f;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma index 8787ecbb9..28eee66dc 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma @@ -12,15 +12,14 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_gen.ma". -include "ground/relocation/tr_id_tls.ma". +include "delayed_updating/substitution/lift_rmap.ma". +include "delayed_updating/substitution/prelift_rmap_id.ma". (* LIFT FOR RELOCATION MAP **************************************************) -(* Constructions with proj_rmap and tr_id ***********************************) +(* Constructions with tr_id *************************************************) lemma lift_rmap_id (p): - (𝐢) = ↑[p]𝐢. + (𝐢) = 🠢[𝐢]p. #p elim p -p // -* [ #n ] #p #IH // qed.