]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_id_pap.ma
index 34f7ca78c6b2c35bfeeae99931221c160e0bbf20..9a406ba8c920086e8e963d86bd823c4e6cec6825 100644 (file)
@@ -19,7 +19,7 @@ include "ground/relocation/tr_id_pushs.ma".
 
 (* Coonstructions with tr_pap ***********************************************)
 
-lemma tr_pap_id (p):
+lemma tr_id_pap (p):
       p = 𝐢@❨p❩.
 #p >(tr_pushs_id p)
 /2 width=1 by tr_pap_pushs_le/