X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fnap.ma;h=ac32304ed352d6fd996c64900ead586effd36fe2;hb=6c52017b15171aa20ddfd01c1bbf3cc22a86c81c;hp=985b3ae26e292b0be8b77d0db3f7fa7d555e4010;hpb=4ac2becfaa45abb18acb2bdf3db5d2587cadb6d4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
index 985b3ae26..ac32304ed 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -22,6 +22,10 @@ lemma tr_nap_unfold (f) (l):
       ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
 // qed.
 
+lemma tr_pap_succ_nap (f) (l):
+      ↑(f@↑❨l❩) = f＠⧣❨↑l❩.
+// qed.
+
 lemma tr_compose_nap (f2) (f1) (l):
       f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
 #f2 #f1 #l