X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_id_pap.ma;h=34f7ca78c6b2c35bfeeae99931221c160e0bbf20;hb=775ab35f714568dfcd672f0dd53a00e1ba7382cd;hp=59256fbbb2cfab01c61153504911eb5fea8a6881;hpb=56092257aa4be8e6d0ae37ee6590f6d3258b0485;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
index 59256fbbb..34f7ca78c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/tr_pap.ma".
-include "ground/relocation/tr_id.ma".
+include "ground/relocation/tr_pap_pushs.ma".
+include "ground/relocation/tr_id_pushs.ma".
 
 (* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
 
@@ -21,6 +21,6 @@ include "ground/relocation/tr_id.ma".
 
 lemma tr_pap_id (p):
       p = 𝐢@❨p❩.
-#p elim p -p //
-#p #IH <tr_id_unfold <tr_pap_succ //
+#p >(tr_pushs_id p)
+/2 width=1 by tr_pap_pushs_le/
 qed.