From: Ferruccio Guidi Date: Wed, 22 Jun 2022 11:38:45 +0000 (+0200) Subject: update in ground X-Git-Tag: make_still_working~56 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=9fe8259fe25c35d33490d94612023f10dc70a603;p=helm.git update in ground + minor corrections --- diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma index 5e607ac37..a9096f7e4 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma @@ -1,8 +1,9 @@ + +(**) (* reverse include *) include "ground/arith/nat_rplus_pplus.ma". +include "ground/relocation/tr_compose_pn.ma". include "ground/relocation/nap.ma". include "ground/notation/functions/apply_2.ma". -include "ground/relocation/tr_compose_pn.ma". -include "ground/relocation/tr_pap_tls.ma". definition tr_xap (f) (l:nat): nat ≝ (⫯f)@↑❨l❩.